# HG changeset patch # User paulson # Date 1034587920 -7200 # Node ID 7f6f0ffc45c3c798304d88732658788e68be45d4 # Parent 46ed3d042ba5444ae4439c2c90c7413c60636564 tidying and reorganization diff -r 46ed3d042ba5 -r 7f6f0ffc45c3 src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Mon Oct 14 10:44:32 2002 +0200 +++ b/src/ZF/Constructible/Datatype_absolute.thy Mon Oct 14 11:32:00 2002 +0200 @@ -425,7 +425,7 @@ done - +text{*This result and the next are unused.*} 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) @@ -577,8 +577,6 @@ done -subsection{*Absoluteness for Some List Operators*} - subsection{*Absoluteness for @{text \}-Closure: the @{term eclose} Operator*} text{*Re-expresses eclose using "iterates"*} @@ -705,8 +703,9 @@ subsection{*Absoluteness for the List Operator @{term length}*} +text{*But it is never used.*} + constdefs - is_length :: "[i=>o,i,i,i] => o" "is_length(M,A,l,n) == \sn[M]. \list_n[M]. \list_sn[M]. @@ -729,7 +728,7 @@ by (simp add: nat_into_M) -subsection {*Absoluteness for @{term nth}*} +subsection {*Absoluteness for the List Operator @{term nth}*} lemma nth_eq_hd_iterates_tl [rule_format]: "xs \ list(A) ==> \n \ nat. nth(n,xs) = hd' (tl'^n (xs))" @@ -828,8 +827,67 @@ by (simp add: Forall_def) + subsection {*Absoluteness for @{term formula_rec}*} +constdefs + + formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i" + --{* the instance of @{term formula_case} in @{term formula_rec}*} + "formula_rec_case(a,b,c,d,h) == + 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))" + +text{*Unfold @{term formula_rec} to @{term formula_rec_case}. + Express @{term formula_rec} without using @{term rank} or @{term Vset}, +neither of which is absolute.*} +lemma (in M_trivial) formula_rec_eq: + "p \ formula ==> + formula_rec(a,b,c,d,p) = + transrec (succ(depth(p)), + \x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p" +apply (simp add: formula_rec_case_def) +apply (induct_tac p) + txt{*Base case for @{term Member}*} + apply (subst transrec, simp add: formula.intros) + txt{*Base case for @{term Equal}*} + apply (subst transrec, simp add: formula.intros) + txt{*Inductive step for @{term Nand}*} + apply (subst transrec) + apply (simp add: succ_Un_distrib formula.intros) +txt{*Inductive step for @{term Forall}*} +apply (subst transrec) +apply (simp add: formula_imp_formula_N formula.intros) +done + + +subsubsection{*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_trivial) depth_closed [intro,simp]: + "p \ formula ==> M(depth(p))" +by (simp add: nat_into_M) + + subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*} constdefs @@ -866,73 +924,17 @@ by (erule formula.cases, simp_all) -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_trivial) depth_closed [intro,simp]: - "p \ formula ==> M(depth(p))" -by (simp add: nat_into_M) - - -subsection {*Absoluteness for @{term formula_rec}*} +subsubsection {*Absoluteness for @{term formula_rec}: Final Results*} constdefs - - formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i" - --{* the instance of @{term formula_case} in @{term formula_rec}*} - "formula_rec_case(a,b,c,d,h) == - 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))" - is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o" --{* predicate to relativize the functional @{term formula_rec}*} "is_formula_rec(M,MH,p,z) == \dp[M]. \i[M]. \f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)" -text{*Unfold @{term formula_rec} to @{term formula_rec_case}. - Express @{term formula_rec} without using @{term rank} or @{term Vset}, -neither of which is absolute.*} -lemma (in M_trivial) formula_rec_eq: - "p \ formula ==> - formula_rec(a,b,c,d,p) = - transrec (succ(depth(p)), - \x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p" -apply (simp add: formula_rec_case_def) -apply (induct_tac p) - txt{*Base case for @{term Member}*} - apply (subst transrec, simp add: formula.intros) - txt{*Base case for @{term Equal}*} - apply (subst transrec, simp add: formula.intros) - txt{*Inductive step for @{term Nand}*} - apply (subst transrec) - apply (simp add: succ_Un_distrib formula.intros) -txt{*Inductive step for @{term Forall}*} -apply (subst transrec) -apply (simp add: formula_imp_formula_N formula.intros) -done - -text{*Sufficient conditions to relative the instance of @{term formula_case} +text{*Sufficient conditions to relativize the instance of @{term formula_case} in @{term formula_rec}*} lemma (in M_datatypes) Relation1_formula_rec_case: "[|Relation2(M, nat, nat, is_a, a); diff -r 46ed3d042ba5 -r 7f6f0ffc45c3 src/ZF/Constructible/Formula.thy --- a/src/ZF/Constructible/Formula.thy Mon Oct 14 10:44:32 2002 +0200 +++ b/src/ZF/Constructible/Formula.thy Mon Oct 14 11:32:00 2002 +0200 @@ -188,6 +188,63 @@ disj_iff_sats imp_iff_sats iff_iff_sats imp_iff_sats ball_iff_sats bex_iff_sats + +subsection{*Arity of a Formula: Maximum Free de Bruijn Index*} + +consts arity :: "i=>i" +primrec + "arity(Member(x,y)) = succ(x) \ succ(y)" + + "arity(Equal(x,y)) = succ(x) \ succ(y)" + + "arity(Nand(p,q)) = arity(p) \ arity(q)" + + "arity(Forall(p)) = Arith.pred(arity(p))" + + +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) + +lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \ arity(q)" +by (simp add: Implies_def) + +lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \ arity(q)" +by (simp add: Iff_def, blast) + +lemma arity_Exists [simp]: "arity(Exists(p)) = Arith.pred(arity(p))" +by (simp add: Exists_def) + + +lemma arity_sats_iff [rule_format]: + "[| p \ formula; extra \ list(A) |] + ==> \env \ list(A). + arity(p) \ length(env) --> + sats(A, p, env @ extra) <-> sats(A, p, env)" +apply (induct_tac p) +apply (simp_all add: Arith.pred_def nth_append Un_least_lt_iff nat_imp_quasinat + split: split_nat_case, auto) +done + +lemma arity_sats1_iff: + "[| arity(p) \ succ(length(env)); p \ formula; x \ A; env \ list(A); + extra \ list(A) |] + ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))" +apply (insert arity_sats_iff [of p extra A "Cons(x,env)"]) +apply simp +done + + +subsection{*Renaming Some de Bruijn Variables*} + constdefs incr_var :: "[i,i]=>i" "incr_var(x,lev) == if xlev \ nat. Forall (incr_bv(p) ` succ(lev)))" -constdefs incr_boundvars :: "i => i" - "incr_boundvars(p) == incr_bv(p)`0" - - lemma [TC]: "x \ nat ==> incr_var(x,lev) \ nat" by (simp add: incr_var_def) lemma incr_bv_type [TC]: "p \ formula ==> incr_bv(p) \ nat -> formula" by (induct_tac p, simp_all) -lemma incr_boundvars_type [TC]: "p \ formula ==> incr_boundvars(p) \ formula" -by (simp add: incr_boundvars_def) - -(*Obviously DPow is closed under complements and finite intersections and -unions. Needs an inductive lemma to allow two lists of parameters to -be combined.*) +text{*Obviously, @{term DPow} is closed under complements and finite +intersections and unions. Needs an inductive lemma to allow two lists of +parameters to be combined.*} lemma sats_incr_bv_iff [rule_format]: "[| p \ formula; env \ list(A); x \ A |] @@ -241,76 +291,6 @@ apply (auto simp add: diff_succ not_lt_iff_le) done -(*UNUSED*) -lemma sats_incr_boundvars_iff: - "[| p \ formula; env \ list(A); x \ A |] - ==> sats(A, incr_boundvars(p), Cons(x,env)) <-> sats(A, p, env)" -apply (insert sats_incr_bv_iff [of p env A x Nil]) -apply (simp add: incr_boundvars_def) -done - -(*UNUSED -lemma formula_add_params [rule_format]: - "[| p \ formula; n \ nat |] - ==> \bvs \ list(A). \env \ list(A). - length(bvs) = n --> - sats(A, iterates(incr_boundvars,n,p), bvs@env) <-> sats(A, p, env)" -apply (induct_tac n, simp, clarify) -apply (erule list.cases) -apply (auto simp add: sats_incr_boundvars_iff) -done -*) - -consts arity :: "i=>i" -primrec - "arity(Member(x,y)) = succ(x) \ succ(y)" - - "arity(Equal(x,y)) = succ(x) \ succ(y)" - - "arity(Nand(p,q)) = arity(p) \ arity(q)" - - "arity(Forall(p)) = nat_case(0, %x. x, arity(p))" - - -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) - -lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \ arity(q)" -by (simp add: Implies_def) - -lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \ arity(q)" -by (simp add: Iff_def, blast) - -lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))" -by (simp add: Exists_def) - - -lemma arity_sats_iff [rule_format]: - "[| p \ formula; extra \ list(A) |] - ==> \env \ list(A). - arity(p) \ length(env) --> - sats(A, p, env @ extra) <-> sats(A, p, env)" -apply (induct_tac p) -apply (simp_all add: nth_append Un_least_lt_iff arity_type nat_imp_quasinat - split: split_nat_case, auto) -done - -lemma arity_sats1_iff: - "[| arity(p) \ succ(length(env)); p \ formula; x \ A; env \ list(A); - extra \ list(A) |] - ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))" -apply (insert arity_sats_iff [of p extra A "Cons(x,env)"]) -apply simp -done (*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*) lemma incr_var_lemma: @@ -336,7 +316,7 @@ apply (induct_tac p) apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff succ_Un_distrib [symmetric] incr_var_lt incr_var_le - Un_commute incr_var_lemma arity_type nat_imp_quasinat + Un_commute incr_var_lemma Arith.pred_def nat_imp_quasinat split: split_nat_case) txt{*the Forall case reduces to linear arithmetic*} prefer 2 @@ -350,24 +330,8 @@ apply (simp add: Un_commute) done -lemma arity_incr_boundvars_eq: - "p \ formula - ==> arity(incr_boundvars(p)) = - (if 0 < arity(p) then succ(arity(p)) else arity(p))" -apply (insert arity_incr_bv_lemma [of p 0]) -apply (simp add: incr_boundvars_def) -done -lemma arity_iterates_incr_boundvars_eq: - "[| p \ formula; n \ nat |] - ==> arity(incr_boundvars^n(p)) = - (if 0 < arity(p) then n #+ arity(p) else arity(p))" -apply (induct_tac n) -apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le) -done - - -subsection{*Renaming all but the first bound variable*} +subsection{*Renaming all but the First de Bruijn Variable*} constdefs incr_bv1 :: "i => i" "incr_bv1(p) == incr_bv(p)`1" @@ -377,7 +341,7 @@ by (simp add: incr_bv1_def) (*For renaming all but the bound variable at level 0*) -lemma sats_incr_bv1_iff [rule_format]: +lemma sats_incr_bv1_iff: "[| p \ formula; env \ list(A); x \ A; y \ A |] ==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <-> sats(A, p, Cons(x,env))" @@ -416,7 +380,10 @@ done -(*Definable powerset operation: Kunen's definition 1.1, page 165.*) + +subsection{*Definable Powerset*} + +text{*The definable powerset operation: Kunen's definition VI 1.1, page 165.*} constdefs DPow :: "i => i" "DPow(A) == {X \ Pow(A). \env \ list(A). \p \ formula. @@ -445,7 +412,7 @@ lemmas DPow_imp_subset = DPowD [THEN conjunct1] -(*Lemma 1.2*) +(*Kunen's Lemma VI 1.2*) lemma "[| p \ formula; env \ list(A); arity(p) \ succ(length(env)) |] ==> {x\A. sats(A, p, Cons(x,env))} \ DPow(A)" by (blast intro: DPowI) diff -r 46ed3d042ba5 -r 7f6f0ffc45c3 src/ZF/Constructible/Rank.thy --- a/src/ZF/Constructible/Rank.thy Mon Oct 14 10:44:32 2002 +0200 +++ b/src/ZF/Constructible/Rank.thy Mon Oct 14 11:32:00 2002 +0200 @@ -666,6 +666,12 @@ +subsection {*Absoluteness of Well-Founded Relations*} + +text{*Relativized to @{term M}: Every well-founded relation is a subset of some +inverse image of an ordinal. Key step is the construction (in @{term M}) of a +rank function.*} + locale M_wfrank = M_trancl + assumes wfrank_separation: "M(r) ==> diff -r 46ed3d042ba5 -r 7f6f0ffc45c3 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Mon Oct 14 10:44:32 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Mon Oct 14 11:32:00 2002 +0200 @@ -204,22 +204,9 @@ lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L] and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L] - and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L] - and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L] - and trancl_closed = M_trancl.trancl_closed [OF M_trancl_L] - and trancl_abs = M_trancl.trancl_abs [OF M_trancl_L] - and wellfounded_on_trancl = M_trancl.wellfounded_on_trancl [OF M_trancl_L] - and wellfounded_trancl = M_trancl.wellfounded_trancl [OF M_trancl_L] - and wfrec_relativize = M_trancl.wfrec_relativize [OF M_trancl_L] - and trans_wfrec_relativize = M_trancl.trans_wfrec_relativize [OF M_trancl_L] and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L] - and trans_eq_pair_wfrec_iff = M_trancl.trans_eq_pair_wfrec_iff [OF M_trancl_L] and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L] -declare rtrancl_closed [intro,simp] -declare rtrancl_abs [simp] -declare trancl_closed [intro,simp] -declare trancl_abs [simp] subsection{*@{term L} is Closed Under the Operator @{term list}*} diff -r 46ed3d042ba5 -r 7f6f0ffc45c3 src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Mon Oct 14 10:44:32 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Mon Oct 14 11:32:00 2002 +0200 @@ -3,7 +3,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory *) -header {*Absoluteness for Well-Founded Relations and Well-Founded Recursion*} +header {*Absoluteness of Well-Founded Recursion*} theory WF_absolute = WFrec: @@ -175,13 +175,8 @@ apply (simp_all add: trancl_type [THEN field_rel_subset]) done -text{*Relativized to M: Every well-founded relation is a subset of some -inverse image of an ordinal. Key step is the construction (in M) of a -rank function.*} - - -text{*absoluteness for wfrec-defined functions.*} +text{*Absoluteness for wfrec-defined functions.*} (*first use is_recfun, then M_is_recfun*)