equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* General Stream domain *} |
5 header {* General Stream domain *} |
6 |
6 |
7 theory Stream |
7 theory Stream |
8 imports HOLCF "~~/src/HOL/Library/Extended_Nat" |
8 imports "../HOLCF" "~~/src/HOL/Library/Extended_Nat" |
9 begin |
9 begin |
10 |
10 |
11 default_sort pcpo |
11 default_sort pcpo |
12 |
12 |
13 domain (unsafe) 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65) |
13 domain (unsafe) 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65) |
790 apply (simp add: sconc_def eSuc_enat) |
790 apply (simp add: sconc_def eSuc_enat) |
791 apply (rule someI2_ex) |
791 apply (rule someI2_ex) |
792 apply (drule ex_sconc, simp) |
792 apply (drule ex_sconc, simp) |
793 apply (rule someI2_ex, auto) |
793 apply (rule someI2_ex, auto) |
794 apply (simp add: i_rt_Suc_forw) |
794 apply (simp add: i_rt_Suc_forw) |
795 apply (rule_tac x="a && x" in exI, auto) |
795 apply (rule_tac x="a && xa" in exI, auto) |
796 apply (case_tac "xa=UU",auto) |
796 apply (case_tac "xaa=UU",auto) |
797 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
797 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
798 apply (drule streams_prefix_lemma1,simp+) |
798 apply (drule streams_prefix_lemma1,simp+) |
799 apply (simp add: sconc_def) |
799 apply (simp add: sconc_def) |
800 done |
800 done |
801 |
801 |