equal
deleted
inserted
replaced
684 (fn _ => |
684 (fn _ => |
685 [ |
685 [ |
686 Asm_simp_tac 1, |
686 Asm_simp_tac 1, |
687 safe_tac HOL_cs, |
687 safe_tac HOL_cs, |
688 subgoal_tac "ia = i" 1, |
688 subgoal_tac "ia = i" 1, |
689 Asm_simp_tac 1, |
689 ALLGOALS Asm_simp_tac |
690 trans_tac 1 |
|
691 ]); |
690 ]); |
692 |
691 |
693 val adm_disj_lemma4 = prove_goal Nat.thy |
692 val adm_disj_lemma4 = prove_goal Nat.thy |
694 "!!Q. !j. i < j --> Q(Y(j)) ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)" |
693 "!!Q. !j. i < j --> Q(Y(j)) ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)" |
695 (fn _ => |
694 (fn _ => |
703 safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]), |
702 safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]), |
704 atac 2, |
703 atac 2, |
705 Asm_simp_tac 1, |
704 Asm_simp_tac 1, |
706 res_inst_tac [("x","i")] exI 1, |
705 res_inst_tac [("x","i")] exI 1, |
707 strip_tac 1, |
706 strip_tac 1, |
708 trans_tac 1 |
707 Simp_tac 1 |
709 ]); |
708 ]); |
710 |
709 |
711 val adm_disj_lemma6 = prove_goal thy |
710 val adm_disj_lemma6 = prove_goal thy |
712 "[| chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==>\ |
711 "[| chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==>\ |
713 \ ? X. chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))" |
712 \ ? X. chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))" |