668 dtac (ax_flat RS spec RS spec RS mp) 1, |
668 dtac (ax_flat RS spec RS spec RS mp) 1, |
669 fast_tac ((HOL_cs addss (simpset() addsimps [minimal]))) 1 |
669 fast_tac ((HOL_cs addss (simpset() addsimps [minimal]))) 1 |
670 ]); |
670 ]); |
671 |
671 |
672 |
672 |
673 qed_goal "chfindom_monofun2cont" thy "monofun f ==> cont(f::'a::chfin=>'b::pcpo)" |
673 Goal "monofun f ==> cont(f::'a::chfin=>'b::pcpo)"; |
674 (fn prems => |
674 by(rtac monocontlub2cont 1); |
675 [ |
675 by( atac 1); |
676 cut_facts_tac prems 1, |
676 by(rtac contlubI 1); |
677 rtac monocontlub2cont 1, |
677 by(strip_tac 1); |
678 atac 1, |
678 by(forward_tac [chfin2finch] 1); |
679 rtac contlubI 1, |
679 by(rtac antisym_less 1); |
680 strip_tac 1, |
680 by( force_tac (HOL_cs addIs [is_ub_thelub,ch2ch_monofun], |
681 forward_tac [chfin2finch] 1, |
681 HOL_ss addsimps [finite_chain_def,maxinch_is_thelub]) 1); |
682 rtac antisym_less 1, |
682 by(dtac (monofun_finch2finch COMP swap_prems_rl) 1); |
683 fast_tac ((HOL_cs addIs [is_ub_thelub,ch2ch_monofun]) |
683 by( atac 1); |
684 addss (HOL_ss addsimps [finite_chain_def,maxinch_is_thelub])) 1, |
684 by(asm_full_simp_tac (HOL_ss addsimps [finite_chain_def]) 1); |
685 dtac (monofun_finch2finch COMP swap_prems_rl) 1, |
685 by(etac conjE 1); |
686 atac 1, |
686 by(etac exE 1); |
687 asm_full_simp_tac (HOL_ss addsimps [finite_chain_def]) 1, |
687 by(asm_full_simp_tac (HOL_ss addsimps [maxinch_is_thelub]) 1); |
688 etac conjE 1, etac exE 1, |
688 by(etac (monofunE RS spec RS spec RS mp) 1); |
689 asm_full_simp_tac (HOL_ss addsimps [maxinch_is_thelub]) 1, |
689 by(etac is_ub_thelub 1); |
690 etac (monofunE RS spec RS spec RS mp) 1, |
690 qed "chfindom_monofun2cont"; |
691 etac is_ub_thelub 1 |
|
692 ]); |
|
693 |
|
694 |
691 |
695 bind_thm ("flatdom_strict2cont",flatdom2monofun RS chfindom_monofun2cont); |
692 bind_thm ("flatdom_strict2cont",flatdom2monofun RS chfindom_monofun2cont); |
696 (* f UU = UU ==> cont (f::'a=>'b::pcpo)" *) |
693 (* f UU = UU ==> cont (f::'a=>'b::pcpo)" *) |