329 by (safe_tac (claset() addSEs [isubE, subchainE])); |
329 by (safe_tac (claset() addSEs [isubE, subchainE])); |
330 by (assume_tac 1); |
330 by (assume_tac 1); |
331 by (Asm_simp_tac 1); |
331 by (Asm_simp_tac 1); |
332 qed "subchain_isub"; |
332 qed "subchain_isub"; |
333 |
333 |
334 Goal |
334 Goal "[|dominate(D,X,Y); subchain(Y,X); islub(D,X,x); islub(D,Y,y); cpo(D); \ |
335 "[|dominate(D,X,Y); subchain(Y,X); islub(D,X,x); islub(D,Y,y); cpo(D); \ |
|
336 \ X:nat->set(D); Y:nat->set(D)|] ==> x = y"; |
335 \ X:nat->set(D); Y:nat->set(D)|] ==> x = y"; |
337 by (blast_tac (claset() addIs [cpo_antisym, dominate_islub, islub_least, |
336 by (blast_tac (claset() addIs [cpo_antisym, dominate_islub, islub_least, |
338 subchain_isub, islub_isub, islub_in]) 1); |
337 subchain_isub, islub_isub, islub_in]) 1); |
339 qed "dominate_islub_eq"; |
338 qed "dominate_islub_eq"; |
340 |
339 |
2154 Goalw [emb_def] |
2153 Goalw [emb_def] |
2155 "[| emb_chain(DD,ee); n:nat |] ==> emb(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))"; |
2154 "[| emb_chain(DD,ee); n:nat |] ==> emb(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))"; |
2156 by (auto_tac (claset() addIs [exI,rho_projpair], simpset())); |
2155 by (auto_tac (claset() addIs [exI,rho_projpair], simpset())); |
2157 qed "emb_rho_emb"; |
2156 qed "emb_rho_emb"; |
2158 |
2157 |
2159 Goal |
2158 Goal "[| emb_chain(DD,ee); n:nat |] ==> \ |
2160 "[| emb_chain(DD,ee); n:nat |] ==> \ |
|
2161 \ rho_proj(DD,ee,n) : cont(Dinf(DD,ee),DD`n)"; |
2159 \ rho_proj(DD,ee,n) : cont(Dinf(DD,ee),DD`n)"; |
2162 by (auto_tac (claset() addIs [rho_projpair,projpair_p_cont], simpset())); |
2160 by (auto_tac (claset() addIs [rho_projpair,projpair_p_cont], simpset())); |
2163 qed "rho_proj_cont"; |
2161 qed "rho_proj_cont"; |
2164 |
2162 |
2165 (*----------------------------------------------------------------------*) |
2163 (*----------------------------------------------------------------------*) |