--- a/src/ZF/AC/AC15_WO6.thy Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/AC/AC15_WO6.thy Tue Aug 27 11:09:35 2002 +0200
@@ -145,7 +145,7 @@
lemma OUN_eq_UN: "Ord(x) ==> (\<Union>a<x. F(a)) = (\<Union>a \<in> x. F(a))"
by (fast intro!: ltI dest!: ltD)
-lemma lemma1:
+lemma AC15_WO6_aux1:
"\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m
==> (\<Union>i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A"
apply (simp add: Ord_Least [THEN OUN_eq_UN])
@@ -155,7 +155,7 @@
intro!: f_subsets_imp_UN_HH_eq_x [THEN Diff_eq_0_iff [THEN iffD1]])
done
-lemma lemma2:
+lemma AC15_WO6_aux2:
"\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m
==> \<forall>x < (LEAST x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> m"
apply (rule oallI)
@@ -163,7 +163,7 @@
apply (frule HH_subset_imp_eq)
apply (erule ssubst)
apply (blast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2])
- (*but can't use del: DiffE despite the obvious conflictc*)
+ (*but can't use del: DiffE despite the obvious conflict*)
done
theorem AC15_WO6: "AC15 ==> WO6"
@@ -178,7 +178,7 @@
apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
apply (simp_all add: ltD)
apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
- elim!: less_Least_subset_x lemma1 lemma2)
+ elim!: less_Least_subset_x AC15_WO6_aux1 AC15_WO6_aux2)
done
--- a/src/ZF/AC/AC17_AC1.thy Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/AC/AC17_AC1.thy Tue Aug 27 11:09:35 2002 +0200
@@ -78,7 +78,7 @@
apply (blast intro: lam_type)
done
-lemma lemma1:
+lemma AC17_AC1_aux1:
"[| \<forall>f \<in> Pow(x) - {0} -> x. \<exists>u \<in> Pow(x) - {0}. f`u\<notin>u;
\<exists>f \<in> Pow(x)-{0}->x.
x - (\<Union>a \<in> (LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,i)={x}).
@@ -94,18 +94,18 @@
apply (blast dest: apply_type)
done
-lemma lemma2:
+lemma AC17_AC1_aux2:
"~ (\<exists>f \<in> Pow(x)-{0}->x. x - F(f) = 0)
==> (\<lambda>f \<in> Pow(x)-{0}->x . x - F(f))
\<in> (Pow(x) -{0} -> x) -> Pow(x) - {0}"
by (fast intro!: lam_type dest!: Diff_eq_0_iff [THEN iffD1])
-lemma lemma3:
+lemma AC17_AC1_aux3:
"[| f`Z \<in> Z; Z \<in> Pow(x)-{0} |]
==> (\<lambda>X \<in> Pow(x)-{0}. {f`X})`Z \<in> Pow(Z)-{0}"
by auto
-lemma lemma4:
+lemma AC17_AC1_aux4:
"\<exists>f \<in> F. f`((\<lambda>f \<in> F. Q(f))`f) \<in> (\<lambda>f \<in> F. Q(f))`f
==> \<exists>f \<in> F. f`Q(f) \<in> Q(f)"
by simp
@@ -117,15 +117,15 @@
apply (case_tac
"\<exists>f \<in> Pow(x)-{0} -> x.
x - (\<Union>a \<in> (LEAST i. HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,a)) = 0")
-apply (erule lemma1, assumption)
-apply (drule lemma2)
+apply (erule AC17_AC1_aux1, assumption)
+apply (drule AC17_AC1_aux2)
apply (erule allE)
apply (drule bspec, assumption)
-apply (drule lemma4)
+apply (drule AC17_AC1_aux4)
apply (erule bexE)
apply (drule apply_type, assumption)
apply (simp add: HH_Least_eq_x del: Diff_iff )
-apply (drule lemma3, assumption)
+apply (drule AC17_AC1_aux3, assumption)
apply (fast dest!: subst_elem [OF _ HH_Least_eq_x [symmetric]]
f_subset_imp_HH_subset elim!: mem_irrefl)
done
@@ -142,11 +142,11 @@
(* AC1 ==> AC2 *)
(* ********************************************************************** *)
-lemma lemma1:
+lemma AC1_AC2_aux1:
"[| f:(\<Pi>X \<in> A. X); B \<in> A; 0\<notin>A |] ==> {f`B} \<subseteq> B Int {f`C. C \<in> A}"
by (fast elim!: apply_type)
-lemma lemma2:
+lemma AC1_AC2_aux2:
"[| pairwise_disjoint(A); B \<in> A; C \<in> A; D \<in> B; D \<in> C |] ==> f`B = f`C"
by (unfold pairwise_disjoint_def, fast)
@@ -156,8 +156,8 @@
apply (rule impI)
apply (elim asm_rl conjE allE exE impE, assumption)
apply (intro exI ballI equalityI)
-prefer 2 apply (rule lemma1, assumption+)
-apply (fast elim!: lemma2 elim: apply_type)
+prefer 2 apply (rule AC1_AC2_aux1, assumption+)
+apply (fast elim!: AC1_AC2_aux2 elim: apply_type)
done
@@ -165,30 +165,30 @@
(* AC2 ==> AC1 *)
(* ********************************************************************** *)
-lemma lemma1: "0\<notin>A ==> 0 \<notin> {B*{B}. B \<in> A}"
+lemma AC2_AC1_aux1: "0\<notin>A ==> 0 \<notin> {B*{B}. B \<in> A}"
by (fast dest!: sym [THEN Sigma_empty_iff [THEN iffD1]])
-lemma lemma2: "[| X*{X} Int C = {y}; X \<in> A |]
+lemma AC2_AC1_aux2: "[| X*{X} Int C = {y}; X \<in> A |]
==> (THE y. X*{X} Int C = {y}): X*A"
apply (rule subst_elem [of y])
apply (blast elim!: equalityE)
apply (auto simp add: singleton_eq_iff)
done
-lemma lemma3:
+lemma AC2_AC1_aux3:
"\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D Int C = {y}
==> (\<lambda>x \<in> A. fst(THE z. (x*{x} Int C = {z}))) \<in> (\<Pi>X \<in> A. X)"
apply (rule lam_type)
apply (drule bspec, blast)
-apply (blast intro: lemma2 fst_type)
+apply (blast intro: AC2_AC1_aux2 fst_type)
done
lemma AC2_AC1: "AC2 ==> AC1"
apply (unfold AC1_def AC2_def pairwise_disjoint_def)
apply (intro allI impI)
apply (elim allE impE)
-prefer 2 apply (fast elim!: lemma3)
-apply (blast intro!: lemma1)
+prefer 2 apply (fast elim!: AC2_AC1_aux3)
+apply (blast intro!: AC2_AC1_aux1)
done
@@ -211,21 +211,21 @@
(* AC4 ==> AC3 *)
(* ********************************************************************** *)
-lemma lemma1: "f \<in> A->B ==> (\<Union>z \<in> A. {z}*f`z) \<subseteq> A*Union(B)"
+lemma AC4_AC3_aux1: "f \<in> A->B ==> (\<Union>z \<in> A. {z}*f`z) \<subseteq> A*Union(B)"
by (fast dest!: apply_type)
-lemma lemma2: "domain(\<Union>z \<in> A. {z}*f(z)) = {a \<in> A. f(a)\<noteq>0}"
+lemma AC4_AC3_aux2: "domain(\<Union>z \<in> A. {z}*f(z)) = {a \<in> A. f(a)\<noteq>0}"
by blast
-lemma lemma3: "x \<in> A ==> (\<Union>z \<in> A. {z}*f(z))``{x} = f(x)"
+lemma AC4_AC3_aux3: "x \<in> A ==> (\<Union>z \<in> A. {z}*f(z))``{x} = f(x)"
by fast
lemma AC4_AC3: "AC4 ==> AC3"
apply (unfold AC3_def AC4_def)
apply (intro allI ballI)
apply (elim allE impE)
-apply (erule lemma1)
-apply (simp add: lemma2 lemma3 cong add: Pi_cong)
+apply (erule AC4_AC3_aux1)
+apply (simp add: AC4_AC3_aux2 AC4_AC3_aux3 cong add: Pi_cong)
done
(* ********************************************************************** *)
@@ -264,18 +264,18 @@
(* AC5 ==> AC4, Rubin & Rubin, p. 11 *)
(* ********************************************************************** *)
-lemma lemma1: "R \<subseteq> A*B ==> (\<lambda>x \<in> R. fst(x)) \<in> R -> A"
+lemma AC5_AC4_aux1: "R \<subseteq> A*B ==> (\<lambda>x \<in> R. fst(x)) \<in> R -> A"
by (fast intro!: lam_type fst_type)
-lemma lemma2: "R \<subseteq> A*B ==> range(\<lambda>x \<in> R. fst(x)) = domain(R)"
+lemma AC5_AC4_aux2: "R \<subseteq> A*B ==> range(\<lambda>x \<in> R. fst(x)) = domain(R)"
by (unfold lam_def, force)
-lemma lemma3: "[| \<exists>f \<in> A->C. P(f,domain(f)); A=B |] ==> \<exists>f \<in> B->C. P(f,B)"
+lemma AC5_AC4_aux3: "[| \<exists>f \<in> A->C. P(f,domain(f)); A=B |] ==> \<exists>f \<in> B->C. P(f,B)"
apply (erule bexE)
apply (frule domain_of_fun, fast)
done
-lemma lemma4: "[| R \<subseteq> A*B; g \<in> C->R; \<forall>x \<in> C. (\<lambda>z \<in> R. fst(z))` (g`x) = x |]
+lemma AC5_AC4_aux4: "[| R \<subseteq> A*B; g \<in> C->R; \<forall>x \<in> C. (\<lambda>z \<in> R. fst(z))` (g`x) = x |]
==> (\<lambda>x \<in> C. snd(g`x)): (\<Pi>x \<in> C. R``{x})"
apply (rule lam_type)
apply (force dest: apply_type)
@@ -284,9 +284,9 @@
lemma AC5_AC4: "AC5 ==> AC4"
apply (unfold AC4_def AC5_def, clarify)
apply (elim allE ballE)
-apply (drule lemma3 [OF _ lemma2], assumption)
-apply (fast elim!: lemma4)
-apply (blast intro: lemma1)
+apply (drule AC5_AC4_aux3 [OF _ AC5_AC4_aux2], assumption)
+apply (fast elim!: AC5_AC4_aux4)
+apply (blast intro: AC5_AC4_aux1)
done
--- a/src/ZF/Constructible/Formula.thy Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy Tue Aug 27 11:09:35 2002 +0200
@@ -164,11 +164,6 @@
==> (P | Q) <-> sats(A, Or(p,q), env)"
by (simp add: sats_Or_iff)
-lemma imp_iff_sats:
- "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
- ==> (P --> Q) <-> sats(A, Implies(p,q), env)"
-by (simp add: sats_Forall_iff)
-
lemma iff_iff_sats:
"[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
==> (P <-> Q) <-> sats(A, Iff(p,q), env)"
@@ -819,8 +814,6 @@
apply (blast intro: doubleton_in_Lset)
done
-lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
-
lemma singleton_in_LLimit:
"[| a: Lset(i); Limit(i) |] ==> {a} : Lset(i)"
apply (erule Limit_LsetE, assumption)
@@ -974,7 +967,7 @@
done
text{*Kunen's VI, 1.12 *}
-lemma Lset_subset_Vset: "i \<in> nat ==> Lset(i) = Vset(i)";
+lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)";
apply (erule nat_induct)
apply (simp add: Vfrom_0)
apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)
--- a/src/ZF/Constructible/Relative.thy Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Tue Aug 27 11:09:35 2002 +0200
@@ -802,14 +802,6 @@
==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
by (simp add: is_nat_case_def)
-lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
- "M(Inl(a)) <-> M(a)"
-by (simp add: Inl_def)
-
-lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
- "M(Inr(a)) <-> M(a)"
-by (simp add: Inr_def)
-
subsection{*Absoluteness for Ordinals*}
text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
--- a/src/ZF/Constructible/Satisfies_absolute.thy Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Tue Aug 27 11:09:35 2002 +0200
@@ -595,8 +595,8 @@
done
lemmas (in M_satisfies)
- satisfies_closed = Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
-and satisfies_abs = Formula_Rec.formula_rec_abs [OF Formula_Rec_M]
+ satisfies_closed' = Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
+and satisfies_abs' = Formula_Rec.formula_rec_abs [OF Formula_Rec_M]
lemma (in M_satisfies) satisfies_closed:
--- a/src/ZF/Induct/FoldSet.ML Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/Induct/FoldSet.ML Tue Aug 27 11:09:35 2002 +0200
@@ -301,7 +301,7 @@
by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
by (etac Finite_induct 1);
by Auto_tac;
-qed "setsum_0";
+qed "setsum_K0";
(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
Goal "[| Finite(C); Finite(D) |] \
--- a/src/ZF/Induct/Multiset.ML Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/Induct/Multiset.ML Tue Aug 27 11:09:35 2002 +0200
@@ -206,7 +206,7 @@
by (res_inst_tac [("x", "{x:A . 0<f`x}")] exI 1);
by (auto_tac (claset() addIs [Collect_subset RS subset_Finite,
funrestrict_type], simpset()));
-qed "normalize_multiset";
+qed "multiset_normalize";
(** Typechecking rules for union and difference of multisets **)
@@ -231,7 +231,7 @@
Goalw [mdiff_def]
"multiset(M) ==> multiset(M -# N)";
-by (res_inst_tac [("A", "mset_of(M)")] normalize_multiset 1);
+by (res_inst_tac [("A", "mset_of(M)")] multiset_normalize 1);
by (asm_simp_tac (simpset() addsimps [multiset_set_of_Finite]) 2);
by (auto_tac (claset(), simpset() addsimps [mset_of_def, multiset_def]));
by (auto_tac (claset() addSIs [lam_type],
--- a/src/ZF/Induct/Tree_Forest.thy Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/Induct/Tree_Forest.thy Tue Aug 27 11:09:35 2002 +0200
@@ -45,7 +45,7 @@
apply (rule Part_subset)
done
-lemma treeI [TC]: "x \<in> forest(A) ==> x \<in> tree_forest(A)"
+lemma treeI' [TC]: "x \<in> forest(A) ==> x \<in> tree_forest(A)"
by (rule forest_subset_TF [THEN subsetD])
lemma TF_equals_Un: "tree(A) \<union> forest(A) = tree_forest(A)"
--- a/src/ZF/Integ/Bin.ML Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/Integ/Bin.ML Tue Aug 27 11:09:35 2002 +0200
@@ -412,10 +412,6 @@
Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
-bind_thms ("NCons_simps",
- [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);
-
-
bind_thms ("bin_arith_extra_simps",
[integ_of_add RS sym, (*invoke bin_add*)
integ_of_minus RS sym, (*invoke bin_minus*)
--- a/src/ZF/UNITY/WFair.ML Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/UNITY/WFair.ML Tue Aug 27 11:09:35 2002 +0200
@@ -387,7 +387,7 @@
by (blast_tac (claset() addIs leadsTo_refl::prems) 1);
by (rtac (major RS leadsTo_induct) 1);
by (REPEAT (blast_tac (claset() addIs prems) 1));
-qed "lemma";
+qed "leadsTo_induct_pre_aux";
val [major, zb_prem, basis_prem, union_prem] = Goal
@@ -399,7 +399,7 @@
by (cut_facts_tac [major] 1);
by (subgoal_tac "(F : za leadsTo zb) & P(za)" 1);
by (etac conjunct2 1);
-by (rtac (major RS lemma) 1);
+by (rtac (major RS leadsTo_induct_pre_aux) 1);
by (blast_tac (claset() addDs [leadsToD2]
addIs [leadsTo_Union,union_prem]) 3);
by (blast_tac (claset() addIs [leadsTo_Trans,basis_prem, leadsTo_Basis]) 2);
@@ -501,7 +501,7 @@
by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
by (auto_tac (claset() addIs [leadsTo_UN],
simpset() delsimps UN_simps addsimps [Int_UN_distrib]));
-qed "lemma1";
+qed "leadsTo_wf_induct_aux";
(** Meta or object quantifier ? **)
Goal "[| wf(r); \
@@ -515,7 +515,7 @@
by (res_inst_tac [("I", "I")] leadsTo_UN 2);
by (REPEAT (assume_tac 2));
by (Clarify_tac 2);
-by (eres_inst_tac [("I", "I")] lemma1 2);
+by (eres_inst_tac [("I", "I")] leadsTo_wf_induct_aux 2);
by (REPEAT (assume_tac 2));
by (rtac equalityI 1);
by Safe_tac;
@@ -602,7 +602,7 @@
\ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)";
by (Clarify_tac 1);
by (Blast_tac 1);
-qed "lemma1";
+qed "leadsTo_123_aux";
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
(* slightly different from the HOL one: B here is bounded *)
@@ -615,7 +615,7 @@
(*Trans*)
by (Clarify_tac 1);
by (res_inst_tac [("x", "Ba Un Bb")] bexI 1);
-by (blast_tac (claset() addIs [lemma1,leadsTo_Un_Un, leadsTo_cancel1,
+by (blast_tac (claset() addIs [leadsTo_123_aux,leadsTo_Un_Un, leadsTo_cancel1,
leadsTo_Un_duplicate]) 1);
by (Blast_tac 1);
(*Union*)
--- a/src/ZF/ex/Limit.thy Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/ex/Limit.thy Tue Aug 27 11:09:35 2002 +0200
@@ -542,12 +542,12 @@
matrix_chain_lub isub_lemma)
done
-lemma lemma1:
+lemma lub_matrix_diag_aux1:
"lub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m))) =
(THE x. islub(D, (\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m)), x))"
by (simp add: lub_def)
-lemma lemma2:
+lemma lub_matrix_diag_aux2:
"lub(D,(\<lambda>n \<in> nat. M`n`n)) =
(THE x. islub(D, (\<lambda>n \<in> nat. M`n`n), x))"
by (simp add: lub_def)
@@ -556,7 +556,7 @@
"[|matrix(D,M); cpo(D)|]
==> lub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m))) =
lub(D,(\<lambda>n \<in> nat. M`n`n))"
-apply (simp (no_asm) add: lemma1 lemma2)
+apply (simp (no_asm) add: lub_matrix_diag_aux1 lub_matrix_diag_aux2)
apply (simp add: islub_def isub_eq)
done
@@ -876,7 +876,7 @@
lemmas id_comp = fun_is_rel [THEN left_comp_id]
and comp_id = fun_is_rel [THEN right_comp_id]
-lemma lemma1:
+lemma projpair_unique_aux1:
"[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p');
rel(cf(D,E),e,e')|] ==> rel(cf(E,D),p',p)"
apply (rule_tac b=p' in
@@ -899,7 +899,7 @@
text{*Proof's very like the previous one. Is there a pattern that
could be exploited?*}
-lemma lemma2:
+lemma projpair_unique_aux2:
"[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p');
rel(cf(E,D),p',p)|] ==> rel(cf(D,E),e,e')"
apply (rule_tac b=e
@@ -923,7 +923,7 @@
lemma projpair_unique:
"[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p')|]
==> (e=e')<->(p=p')"
-by (blast intro: cpo_antisym lemma1 lemma2 cpo_cf cont_cf
+by (blast intro: cpo_antisym projpair_unique_aux1 projpair_unique_aux2 cpo_cf cont_cf
dest: projpair_ep_cont)
(* Slightly different, more asms, since THE chooses the unique element. *)
@@ -1763,7 +1763,7 @@
(* 32 vs 61, using safe_tac with imp in asm would be unfortunate (5steps) *)
-lemma lemma1:
+lemma eps1_aux1:
"[|m le n; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
==> rel(DD`n,e_less(DD,ee,m,n)`(x`m),x`n)"
apply (erule rev_mp) (* For induction proof *)
@@ -1807,7 +1807,7 @@
(* 18 vs 40 *)
-lemma lemma2:
+lemma eps1_aux2:
"[|n le m; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
==> rel(DD`n,e_gr(DD,ee,m,n)`(x`m),x`n)"
apply (erule rev_mp) (* For induction proof *)
@@ -1835,7 +1835,7 @@
"[|emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
==> rel(DD`n,eps(DD,ee,m,n)`(x`m),x`n)"
apply (simp add: eps_def)
-apply (blast intro: lemma1 not_le_iff_lt [THEN iffD1, THEN leI, THEN lemma2]
+apply (blast intro: eps1_aux1 not_le_iff_lt [THEN iffD1, THEN leI, THEN eps1_aux2]
nat_into_Ord)
done
@@ -1894,7 +1894,7 @@
"[| emb_chain(DD,ee); n \<in> nat |] ==> emb(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))"
by (auto simp add: emb_def intro: exI rho_projpair)
-lemma commuteI: "[| emb_chain(DD,ee); n \<in> nat |]
+lemma rho_proj_cont: "[| emb_chain(DD,ee); n \<in> nat |]
==> rho_proj(DD,ee,n) \<in> cont(Dinf(DD,ee),DD`n)"
by (auto intro: rho_projpair projpair_p_cont)