# HG changeset patch # User paulson # Date 1027094791 -7200 # Node ID 1cadd412da48c887793b70323e5e29cdba98f0aa # Parent 6e5f4d911435877a75f5c9afd528db32568c4265 Towards relativization and absoluteness of formula_rec diff -r 6e5f4d911435 -r 1cadd412da48 src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Fri Jul 19 13:29:22 2002 +0200 +++ b/src/ZF/Constructible/Datatype_absolute.thy Fri Jul 19 18:06:31 2002 +0200 @@ -21,7 +21,7 @@ "[|i \ nat; j \ nat; bnd_mono(D,h)|] ==> i \ j --> h^i(0) \ h^j(0)" apply (rule_tac m=i and n=j in diff_induct, simp_all) apply (blast del: subsetI - intro: bnd_mono_iterates_subset bnd_monoD2 [of concl: h] ) + intro: bnd_mono_iterates_subset bnd_monoD2 [of concl: h]) done lemma directed_iterates: "bnd_mono(D,h) ==> directed({h^n (0). n\nat})" @@ -63,7 +63,7 @@ apply (rule ballI) apply (induct_tac n, simp_all) apply (rule subset_trans [of _ "h(lfp(D,h))"]) - apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset] ) + apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset]) apply (erule lfp_lemma2) done @@ -212,7 +212,7 @@ subsection {*formulas without univ*} lemma formula_fun_bnd_mono: - "bnd_mono(univ(0), \X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))" + "bnd_mono(univ(0), \X. ((nat*nat) + (nat*nat)) + (X*X + X))" apply (rule bnd_monoI) apply (intro subset_refl zero_subset_univ A_subset_univ sum_subset_univ Sigma_subset_univ nat_subset_univ) @@ -220,25 +220,25 @@ done lemma formula_fun_contin: - "contin(\X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))" + "contin(\X. ((nat*nat) + (nat*nat)) + (X*X + X))" by (intro sum_contin prod_contin id_contin const_contin) text{*Re-expresses formulas using sum and product*} lemma formula_eq_lfp2: - "formula = lfp(univ(0), \X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))" + "formula = lfp(univ(0), \X. ((nat*nat) + (nat*nat)) + (X*X + X))" apply (simp add: formula_def) apply (rule equalityI) apply (rule lfp_lowerbound) prefer 2 apply (rule lfp_subset) apply (clarify, subst lfp_unfold [OF formula_fun_bnd_mono]) - apply (simp add: Member_def Equal_def Neg_def And_def Forall_def) + apply (simp add: Member_def Equal_def Nand_def Forall_def) apply blast txt{*Opposite inclusion*} apply (rule lfp_lowerbound) prefer 2 apply (rule lfp_subset, clarify) apply (subst lfp_unfold [OF formula.bnd_mono, simplified]) -apply (simp add: Member_def Equal_def Neg_def And_def Forall_def) +apply (simp add: Member_def Equal_def Nand_def Forall_def) apply (elim sumE SigmaE, simp_all) apply (blast intro: datatype_univs dest: lfp_subset [THEN subsetD])+ done @@ -246,7 +246,7 @@ text{*Re-expresses formulas using "iterates", no univ.*} lemma formula_eq_Union: "formula = - (\n\nat. (\X. ((nat*nat) + (nat*nat)) + (X + (X*X + X))) ^ n (0))" + (\n\nat. (\X. ((nat*nat) + (nat*nat)) + (X*X + X)) ^ n (0))" by (simp add: formula_eq_lfp2 lfp_eq_Union formula_fun_bnd_mono formula_fun_contin) @@ -254,16 +254,16 @@ constdefs is_formula_functor :: "[i=>o,i,i] => o" "is_formula_functor(M,X,Z) == - \nat'[M]. \natnat[M]. \natnatsum[M]. \XX[M]. \X3[M]. \X4[M]. + \nat'[M]. \natnat[M]. \natnatsum[M]. \XX[M]. \X3[M]. omega(M,nat') & cartprod(M,nat',nat',natnat) & is_sum(M,natnat,natnat,natnatsum) & - cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & is_sum(M,X,X3,X4) & - is_sum(M,natnatsum,X4,Z)" + cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & + is_sum(M,natnatsum,X3,Z)" lemma (in M_axioms) formula_functor_abs [simp]: "[| M(X); M(Z) |] ==> is_formula_functor(M,X,Z) <-> - Z = ((nat*nat) + (nat*nat)) + (X + (X*X + X))" + Z = ((nat*nat) + (nat*nat)) + (X*X + X)" by (simp add: is_formula_functor_def) @@ -429,7 +429,7 @@ subsubsection{*Absoluteness of Formulas*} lemma (in M_datatypes) formula_replacement2': - "strong_replacement(M, \n y. n\nat & y = (\X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0))" + "strong_replacement(M, \n y. n\nat & y = (\X. ((nat*nat) + (nat*nat)) + (X*X + X))^n (0))" apply (insert formula_replacement2) apply (rule strong_replacement_cong [THEN iffD1]) apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]]) @@ -447,11 +447,11 @@ lemma (in M_datatypes) is_formula_n_abs [simp]: "[|n\nat; M(Z)|] ==> is_formula_n(M,n,Z) <-> - Z = (\X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0)" + Z = (\X. ((nat*nat) + (nat*nat)) + (X*X + X))^n (0)" apply (insert formula_replacement1) apply (simp add: is_formula_n_def relativize1_def nat_into_M iterates_abs [of "is_formula_functor(M)" _ - "\X. ((nat*nat) + (nat*nat)) + (X + (X*X + X))"]) + "\X. ((nat*nat) + (nat*nat)) + (X*X + X)"]) done lemma (in M_datatypes) mem_formula_abs [simp]: @@ -609,7 +609,7 @@ text{*Proof is trivial since @{term length} returns natural numbers.*} lemma (in M_triv_axioms) length_closed [intro,simp]: "l \ list(A) ==> M(length(l))" -by (simp add: nat_into_M ) +by (simp add: nat_into_M) subsection {*Absoluteness for @{term nth}*} @@ -661,4 +661,336 @@ done + + +subsection{*Relativization and Absoluteness for the @{term formula} Constructors*} + +constdefs + is_Member :: "[i=>o,i,i,i] => o" + --{* because @{term "Member(x,y) \ Inl(Inl(\x,y\))"}*} + "is_Member(M,x,y,Z) == + \p[M]. \u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" + +lemma (in M_triv_axioms) Member_abs [simp]: + "[|M(x); M(y); M(Z)|] ==> is_Member(M,x,y,Z) <-> (Z = Member(x,y))" +by (simp add: is_Member_def Member_def) + +lemma (in M_triv_axioms) Member_in_M_iff [iff]: + "M(Member(x,y)) <-> M(x) & M(y)" +by (simp add: Member_def) + +constdefs + is_Equal :: "[i=>o,i,i,i] => o" + --{* because @{term "Equal(x,y) \ Inl(Inr(\x,y\))"}*} + "is_Equal(M,x,y,Z) == + \p[M]. \u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" + +lemma (in M_triv_axioms) Equal_abs [simp]: + "[|M(x); M(y); M(Z)|] ==> is_Equal(M,x,y,Z) <-> (Z = Equal(x,y))" +by (simp add: is_Equal_def Equal_def) + +lemma (in M_triv_axioms) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)" +by (simp add: Equal_def) + +constdefs + is_Nand :: "[i=>o,i,i,i] => o" + --{* because @{term "Nand(x,y) \ Inr(Inl(\x,y\))"}*} + "is_Nand(M,x,y,Z) == + \p[M]. \u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" + +lemma (in M_triv_axioms) Nand_abs [simp]: + "[|M(x); M(y); M(Z)|] ==> is_Nand(M,x,y,Z) <-> (Z = Nand(x,y))" +by (simp add: is_Nand_def Nand_def) + +lemma (in M_triv_axioms) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)" +by (simp add: Nand_def) + +constdefs + is_Forall :: "[i=>o,i,i] => o" + --{* because @{term "Forall(x) \ Inr(Inr(p))"}*} + "is_Forall(M,p,Z) == \u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)" + +lemma (in M_triv_axioms) Forall_abs [simp]: + "[|M(x); M(Z)|] ==> is_Forall(M,x,Z) <-> (Z = Forall(x))" +by (simp add: is_Forall_def Forall_def) + +lemma (in M_triv_axioms) Forall_in_M_iff [iff]: "M(Forall(x)) <-> M(x)" +by (simp add: Forall_def) + + +subsection {*Absoluteness for @{term formula_rec}*} + +subsubsection{*@{term quasiformula}: For Case-Splitting with @{term formula_case'}*} + +constdefs + + quasiformula :: "i => o" + "quasiformula(p) == + (\x y. p = Member(x,y)) | + (\x y. p = Equal(x,y)) | + (\x y. p = Nand(x,y)) | + (\x. p = Forall(x))" + + is_quasiformula :: "[i=>o,i] => o" + "is_quasiformula(M,p) == + (\x[M]. \y[M]. is_Member(M,x,y,p)) | + (\x[M]. \y[M]. is_Equal(M,x,y,p)) | + (\x[M]. \y[M]. is_Nand(M,x,y,p)) | + (\x[M]. is_Forall(M,x,p))" + +lemma [iff]: "quasiformula(Member(x,y))" +by (simp add: quasiformula_def) + +lemma [iff]: "quasiformula(Equal(x,y))" +by (simp add: quasiformula_def) + +lemma [iff]: "quasiformula(Nand(x,y))" +by (simp add: quasiformula_def) + +lemma [iff]: "quasiformula(Forall(x))" +by (simp add: quasiformula_def) + +lemma formula_imp_quasiformula: "p \ formula ==> quasiformula(p)" +by (erule formula.cases, simp_all) + +lemma (in M_triv_axioms) quasiformula_abs [simp]: + "M(z) ==> is_quasiformula(M,z) <-> quasiformula(z)" +by (auto simp add: is_quasiformula_def quasiformula_def) + +constdefs + + formula_case' :: "[[i,i]=>i, [i,i]=>i, [i,i]=>i, i=>i, i] => i" + --{*A version of @{term formula_case} that's always defined.*} + "formula_case'(a,b,c,d,p) == + if quasiformula(p) then formula_case(a,b,c,d,p) else 0" + + is_formula_case :: + "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o" + --{*Returns 0 for non-formulas*} + "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == + (\x[M]. \y[M]. is_Member(M,x,y,p) --> is_a(x,y,z)) & + (\x[M]. \y[M]. is_Equal(M,x,y,p) --> is_b(x,y,z)) & + (\x[M]. \y[M]. is_Nand(M,x,y,p) --> is_c(x,y,z)) & + (\x[M]. is_Forall(M,x,p) --> is_d(x,z)) & + (is_quasiformula(M,p) | empty(M,z))" + +subsubsection{*@{term formula_case'}, the Modified Version of @{term formula_case}*} + +lemma formula_case'_Member [simp]: + "formula_case'(a,b,c,d,Member(x,y)) = a(x,y)" +by (simp add: formula_case'_def) + +lemma formula_case'_Equal [simp]: + "formula_case'(a,b,c,d,Equal(x,y)) = b(x,y)" +by (simp add: formula_case'_def) + +lemma formula_case'_Nand [simp]: + "formula_case'(a,b,c,d,Nand(x,y)) = c(x,y)" +by (simp add: formula_case'_def) + +lemma formula_case'_Forall [simp]: + "formula_case'(a,b,c,d,Forall(x)) = d(x)" +by (simp add: formula_case'_def) + +lemma non_formula_case: "~ quasiformula(x) ==> formula_case'(a,b,c,d,x) = 0" +by (simp add: quasiformula_def formula_case'_def) + +lemma formula_case'_eq_formula_case [simp]: + "p \ formula ==>formula_case'(a,b,c,d,p) = formula_case(a,b,c,d,p)" +by (erule formula.cases, simp_all) + +lemma (in M_axioms) formula_case'_closed [intro,simp]: + "[|M(p); \x[M]. \y[M]. M(a(x,y)); + \x[M]. \y[M]. M(b(x,y)); + \x[M]. \y[M]. M(c(x,y)); + \x[M]. M(d(x))|] ==> M(formula_case'(a,b,c,d,p))" +apply (case_tac "quasiformula(p)") + apply (simp add: quasiformula_def, force) +apply (simp add: non_formula_case) +done + +lemma (in M_triv_axioms) formula_case_abs [simp]: + "[| relativize2(M,is_a,a); relativize2(M,is_b,b); + relativize2(M,is_c,c); relativize1(M,is_d,d); M(p); M(z) |] + ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <-> + z = formula_case'(a,b,c,d,p)" +apply (case_tac "quasiformula(p)") + prefer 2 + apply (simp add: is_formula_case_def non_formula_case) + apply (force simp add: quasiformula_def) +apply (simp add: quasiformula_def is_formula_case_def) +apply (elim disjE exE) + apply (simp_all add: relativize1_def relativize2_def) +done + + +subsubsection{*Towards Absoluteness of @{term formula_rec}*} + +consts depth :: "i=>i" +primrec + "depth(Member(x,y)) = 0" + "depth(Equal(x,y)) = 0" + "depth(Nand(p,q)) = succ(depth(p) \ depth(q))" + "depth(Forall(p)) = succ(depth(p))" + +lemma depth_type [TC]: "p \ formula ==> depth(p) \ nat" +by (induct_tac p, simp_all) + + +constdefs + formula_N :: "i => i" + "formula_N(n) == (\X. ((nat*nat) + (nat*nat)) + (X*X + X)) ^ n (0)" + +lemma Member_in_formula_N [simp]: + "Member(x,y) \ formula_N(succ(n)) <-> x \ nat & y \ nat" +by (simp add: formula_N_def Member_def) + +lemma Equal_in_formula_N [simp]: + "Equal(x,y) \ formula_N(succ(n)) <-> x \ nat & y \ nat" +by (simp add: formula_N_def Equal_def) + +lemma Nand_in_formula_N [simp]: + "Nand(x,y) \ formula_N(succ(n)) <-> x \ formula_N(n) & y \ formula_N(n)" +by (simp add: formula_N_def Nand_def) + +lemma Forall_in_formula_N [simp]: + "Forall(x) \ formula_N(succ(n)) <-> x \ formula_N(n)" +by (simp add: formula_N_def Forall_def) + +text{*These two aren't simprules because they reveal the underlying +formula representation.*} +lemma formula_N_0: "formula_N(0) = 0" +by (simp add: formula_N_def) + +lemma formula_N_succ: + "formula_N(succ(n)) = + ((nat*nat) + (nat*nat)) + (formula_N(n) * formula_N(n) + formula_N(n))" +by (simp add: formula_N_def) + +lemma formula_N_imp_formula: + "[| p \ formula_N(n); n \ nat |] ==> p \ formula" +by (force simp add: formula_eq_Union formula_N_def) + +lemma formula_N_imp_depth_lt [rule_format]: + "n \ nat ==> \p \ formula_N(n). depth(p) < n" +apply (induct_tac n) +apply (auto simp add: formula_N_0 formula_N_succ + depth_type formula_N_imp_formula Un_least_lt_iff + Member_def [symmetric] Equal_def [symmetric] + Nand_def [symmetric] Forall_def [symmetric]) +done + +lemma formula_imp_formula_N [rule_format]: + "p \ formula ==> \n\nat. depth(p) < n --> p \ formula_N(n)" +apply (induct_tac p) +apply (simp_all add: succ_Un_distrib Un_least_lt_iff) +apply (force elim: natE)+ +done + +lemma formula_N_imp_eq_depth: + "[|n \ nat; p \ formula_N(n); p \ formula_N(succ(n))|] + ==> n = depth(p)" +apply (rule le_anti_sym) + prefer 2 apply (simp add: formula_N_imp_depth_lt) +apply (frule formula_N_imp_formula, simp) +apply (simp add: not_lt_iff_le [symmetric]) +apply (blast intro: formula_imp_formula_N) +done + + + +lemma formula_N_mono [rule_format]: + "[| m \ nat; n \ nat |] ==> m\n --> formula_N(m) \ formula_N(n)" +apply (rule_tac m = m and n = n in diff_induct) +apply (simp_all add: formula_N_0 formula_N_succ, blast) +done + +lemma formula_N_distrib: + "[| m \ nat; n \ nat |] ==> formula_N(m \ n) = formula_N(m) \ formula_N(n)" +apply (rule_tac i = m and j = n in Ord_linear_le, auto) +apply (simp_all add: subset_Un_iff [THEN iffD1] subset_Un_iff2 [THEN iffD1] + le_imp_subset formula_N_mono) +done + +lemma Nand_in_formula_N: + "[|p \ formula; q \ formula|] + ==> Nand(p,q) \ formula_N(succ(succ(depth(p))) \ succ(succ(depth(q))))" +by (simp add: succ_Un_distrib [symmetric] formula_imp_formula_N le_Un_iff) + + +text{*Express @{term formula_rec} without using @{term rank} or @{term Vset}, +neither of which is absolute.*} +lemma (in M_triv_axioms) formula_rec_eq: + "p \ formula ==> + formula_rec(a,b,c,d,p) = + transrec (succ(depth(p)), + \x h. Lambda (formula_N(x), + formula_case' (a, b, + \u v. c(u, v, h ` succ(depth(u)) ` u, + h ` succ(depth(v)) ` v), + \u. d(u, h ` succ(depth(u)) ` u)))) + ` p" +apply (induct_tac p) +txt{*Base case for @{term Member}*} +apply (subst transrec, simp) +txt{*Base case for @{term Equal}*} +apply (subst transrec, simp) +txt{*Inductive step for @{term Nand}*} +apply (subst transrec) +apply (simp add: succ_Un_distrib Nand_in_formula_N) +txt{*Inductive step for @{term Forall}*} +apply (subst transrec) +apply (simp add: formula_imp_formula_N) +done + + +constdefs + is_formula_N :: "[i=>o,i,i] => o" + "is_formula_N(M,n,Z) == + \zero[M]. \sn[M]. \msn[M]. + empty(M,zero) & + successor(M,n,sn) & membership(M,sn,msn) & + is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)" + + +lemma (in M_datatypes) formula_N_abs [simp]: + "[|n\nat; M(Z)|] + ==> is_formula_N(M,n,Z) <-> Z = formula_N(n)" +apply (insert formula_replacement1) +apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M + iterates_abs [of "is_formula_functor(M)" _ + "\X. ((nat*nat) + (nat*nat)) + (X*X + X)"]) +done + +lemma (in M_datatypes) formula_N_closed [intro,simp]: + "n\nat ==> M(formula_N(n))" +apply (insert formula_replacement1) +apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M + iterates_closed [of "is_formula_functor(M)"]) +done + +subsection{*Absoluteness for the Formula Operator @{term depth}*} +constdefs + + is_depth :: "[i=>o,i,i] => o" + "is_depth(M,p,n) == + \sn[M]. \formula_n[M]. \formula_sn[M]. + is_formula_N(M,n,formula_n) & p \ formula_n & + successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \ formula_sn" + + +lemma (in M_datatypes) depth_abs [simp]: + "[|p \ formula; n \ nat|] ==> is_depth(M,p,n) <-> n = depth(p)" +apply (subgoal_tac "M(p) & M(n)") + prefer 2 apply (blast dest: transM) +apply (simp add: is_depth_def) +apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth + dest: formula_N_imp_depth_lt) +done + +text{*Proof is trivial since @{term depth} returns natural numbers.*} +lemma (in M_triv_axioms) depth_closed [intro,simp]: + "p \ formula ==> M(depth(p))" +by (simp add: nat_into_M) + end diff -r 6e5f4d911435 -r 1cadd412da48 src/ZF/Constructible/Formula.thy --- a/src/ZF/Constructible/Formula.thy Fri Jul 19 13:29:22 2002 +0200 +++ b/src/ZF/Constructible/Formula.thy Fri Jul 19 18:06:31 2002 +0200 @@ -11,17 +11,22 @@ datatype "formula" = Member ("x: nat", "y: nat") | Equal ("x: nat", "y: nat") - | Neg ("p: formula") - | And ("p: formula", "q: formula") + | Nand ("p: formula", "q: formula") | Forall ("p: formula") declare formula.intros [TC] +constdefs Neg :: "i=>i" + "Neg(p) == Nand(p,p)" + +constdefs And :: "[i,i]=>i" + "And(p,q) == Neg(Nand(p,q))" + constdefs Or :: "[i,i]=>i" - "Or(p,q) == Neg(And(Neg(p),Neg(q)))" + "Or(p,q) == Nand(Neg(p),Neg(q))" constdefs Implies :: "[i,i]=>i" - "Implies(p,q) == Neg(And(p,Neg(q)))" + "Implies(p,q) == Nand(p,Neg(q))" constdefs Iff :: "[i,i]=>i" "Iff(p,q) == And(Implies(p,q), Implies(q,p))" @@ -29,6 +34,12 @@ constdefs Exists :: "i=>i" "Exists(p) == Neg(Forall(Neg(p)))"; +lemma Neg_type [TC]: "p \ formula ==> Neg(p) \ formula" +by (simp add: Neg_def) + +lemma And_type [TC]: "[| p \ formula; q \ formula |] ==> And(p,q) \ formula" +by (simp add: And_def) + lemma Or_type [TC]: "[| p \ formula; q \ formula |] ==> Or(p,q) \ formula" by (simp add: Or_def) @@ -52,11 +63,8 @@ "satisfies(A,Equal(x,y)) = (\env \ list(A). bool_of_o (nth(x,env) = nth(y,env)))" - "satisfies(A,Neg(p)) = - (\env \ list(A). not(satisfies(A,p)`env))" - - "satisfies(A,And(p,q)) = - (\env \ list(A). (satisfies(A,p)`env) and (satisfies(A,q)`env))" + "satisfies(A,Nand(p,q)) = + (\env \ list(A). not ((satisfies(A,p)`env) and (satisfies(A,q)`env)))" "satisfies(A,Forall(p)) = (\env \ list(A). bool_of_o (\x\A. satisfies(A,p) ` (Cons(x,env)) = 1))" @@ -78,15 +86,10 @@ ==> sats(A, Equal(x,y), env) <-> nth(x,env) = nth(y,env)" by simp -lemma sats_Neg_iff [simp]: +lemma sats_Nand_iff [simp]: "env \ list(A) - ==> sats(A, Neg(p), env) <-> ~ sats(A,p,env)" -by (simp add: Bool.not_def cond_def) - -lemma sats_And_iff [simp]: - "env \ list(A) - ==> (sats(A, And(p,q), env)) <-> sats(A,p,env) & sats(A,q,env)" -by (simp add: Bool.and_def cond_def) + ==> (sats(A, Nand(p,q), env)) <-> ~ (sats(A,p,env) & sats(A,q,env))" +by (simp add: Bool.and_def Bool.not_def cond_def) lemma sats_Forall_iff [simp]: "env \ list(A) @@ -97,6 +100,16 @@ subsection{*Dividing line between primitive and derived connectives*} +lemma sats_Neg_iff [simp]: + "env \ list(A) + ==> sats(A, Neg(p), env) <-> ~ sats(A,p,env)" +by (simp add: Neg_def) + +lemma sats_And_iff [simp]: + "env \ list(A) + ==> (sats(A, And(p,q), env)) <-> sats(A,p,env) & sats(A,q,env)" +by (simp add: And_def) + lemma sats_Or_iff [simp]: "env \ list(A) ==> (sats(A, Or(p,q), env)) <-> sats(A,p,env) | sats(A,q,env)" @@ -194,11 +207,8 @@ "incr_bv(Equal(x,y)) = (\lev \ nat. Equal (incr_var(x,lev), incr_var(y,lev)))" - "incr_bv(Neg(p)) = - (\lev \ nat. Neg(incr_bv(p)`lev))" - - "incr_bv(And(p,q)) = - (\lev \ nat. And (incr_bv(p)`lev, incr_bv(q)`lev))" + "incr_bv(Nand(p,q)) = + (\lev \ nat. Nand (incr_bv(p)`lev, incr_bv(q)`lev))" "incr_bv(Forall(p)) = (\lev \ nat. Forall (incr_bv(p) ` succ(lev)))" @@ -257,9 +267,7 @@ "arity(Equal(x,y)) = succ(x) \ succ(y)" - "arity(Neg(p)) = arity(p)" - - "arity(And(p,q)) = arity(p) \ arity(q)" + "arity(Nand(p,q)) = arity(p) \ arity(q)" "arity(Forall(p)) = nat_case(0, %x. x, arity(p))" @@ -267,6 +275,12 @@ lemma arity_type [TC]: "p \ formula ==> arity(p) \ nat" by (induct_tac p, simp_all) +lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)" +by (simp add: Neg_def) + +lemma arity_And [simp]: "arity(And(p,q)) = arity(p) \ arity(q)" +by (simp add: And_def) + lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \ arity(q)" by (simp add: Or_def) diff -r 6e5f4d911435 -r 1cadd412da48 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Fri Jul 19 13:29:22 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Fri Jul 19 18:06:31 2002 +0200 @@ -874,20 +874,19 @@ constdefs formula_functor_fm :: "[i,i]=>i" (* "is_formula_functor(M,X,Z) == - \nat'[M]. \natnat[M]. \natnatsum[M]. \XX[M]. \X3[M]. \X4[M]. - 5 4 3 2 1 0 + \nat'[M]. \natnat[M]. \natnatsum[M]. \XX[M]. \X3[M]. + 4 3 2 1 0 omega(M,nat') & cartprod(M,nat',nat',natnat) & is_sum(M,natnat,natnat,natnatsum) & - cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & is_sum(M,X,X3,X4) & - is_sum(M,natnatsum,X4,Z)" *) + cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & + is_sum(M,natnatsum,X3,Z)" *) "formula_functor_fm(X,Z) == - Exists(Exists(Exists(Exists(Exists(Exists( - And(omega_fm(5), - And(cartprod_fm(5,5,4), - And(sum_fm(4,4,3), - And(cartprod_fm(X#+6,X#+6,2), - And(sum_fm(2,X#+6,1), - And(sum_fm(X#+6,1,0), sum_fm(3,0,Z#+6)))))))))))))" + Exists(Exists(Exists(Exists(Exists( + And(omega_fm(4), + And(cartprod_fm(4,4,3), + And(sum_fm(3,3,2), + And(cartprod_fm(X#+5,X#+5,1), + And(sum_fm(1,X#+5,0), sum_fm(2,0,Z#+5)))))))))))" lemma formula_functor_type [TC]: "[| x \ nat; y \ nat |] ==> formula_functor_fm(x,y) \ formula"