equal
deleted
inserted
replaced
900 lemma take_lemma_less1: |
900 lemma take_lemma_less1: |
901 assumes "!! n. seq_take n$s1 << seq_take n$s2" |
901 assumes "!! n. seq_take n$s1 << seq_take n$s2" |
902 shows "s1<<s2" |
902 shows "s1<<s2" |
903 apply (rule_tac t="s1" in seq.reach [THEN subst]) |
903 apply (rule_tac t="s1" in seq.reach [THEN subst]) |
904 apply (rule_tac t="s2" in seq.reach [THEN subst]) |
904 apply (rule_tac t="s2" in seq.reach [THEN subst]) |
905 apply (rule fix_def2 [THEN ssubst]) |
|
906 apply (subst contlub_cfun_fun) |
|
907 apply (rule chain_iterate) |
|
908 apply (subst contlub_cfun_fun) |
|
909 apply (rule chain_iterate) |
|
910 apply (rule lub_mono) |
905 apply (rule lub_mono) |
911 apply (rule chain_iterate [THEN ch2ch_Rep_CFunL]) |
906 apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL]) |
912 apply (rule chain_iterate [THEN ch2ch_Rep_CFunL]) |
907 apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL]) |
913 apply (rule prems [unfolded seq.take_def]) |
908 apply (rule assms) |
914 done |
909 done |
915 |
910 |
916 |
911 |
917 lemma take_lemma_less: "(!n. seq_take n$x << seq_take n$x') = (x << x')" |
912 lemma take_lemma_less: "(!n. seq_take n$x << seq_take n$x') = (x << x')" |
918 apply (rule iffI) |
913 apply (rule iffI) |