21 by (safe_tac type_cs); |
21 by (safe_tac type_cs); |
22 be (XH_to_E ListsXH) 1; |
22 be (XH_to_E ListsXH) 1; |
23 by (EQgen_tac list_ss [] 1); |
23 by (EQgen_tac list_ss [] 1); |
24 by (simp_tac list_ss 1); |
24 by (simp_tac list_ss 1); |
25 by (fast_tac ccl_cs 1); |
25 by (fast_tac ccl_cs 1); |
26 val map_comp = result(); |
26 qed "map_comp"; |
27 |
27 |
28 (*** Mapping the identity function leaves a list unchanged ***) |
28 (*** Mapping the identity function leaves a list unchanged ***) |
29 |
29 |
30 val prems = goal Stream.thy "l:Lists(A) ==> map(%x.x,l) = l"; |
30 val prems = goal Stream.thy "l:Lists(A) ==> map(%x.x,l) = l"; |
31 by (eq_coinduct3_tac |
31 by (eq_coinduct3_tac |
33 by (fast_tac (ccl_cs addSIs prems) 1); |
33 by (fast_tac (ccl_cs addSIs prems) 1); |
34 by (safe_tac type_cs); |
34 by (safe_tac type_cs); |
35 be (XH_to_E ListsXH) 1; |
35 be (XH_to_E ListsXH) 1; |
36 by (EQgen_tac list_ss [] 1); |
36 by (EQgen_tac list_ss [] 1); |
37 by (fast_tac ccl_cs 1); |
37 by (fast_tac ccl_cs 1); |
38 val map_id = result(); |
38 qed "map_id"; |
39 |
39 |
40 (*** Mapping distributes over append ***) |
40 (*** Mapping distributes over append ***) |
41 |
41 |
42 val prems = goal Stream.thy |
42 val prems = goal Stream.thy |
43 "[| l:Lists(A); m:Lists(A) |] ==> map(f,l@m) = map(f,l) @ map(f,m)"; |
43 "[| l:Lists(A); m:Lists(A) |] ==> map(f,l@m) = map(f,l) @ map(f,m)"; |
48 be (XH_to_E ListsXH) 1; |
48 be (XH_to_E ListsXH) 1; |
49 by (EQgen_tac list_ss [] 1); |
49 by (EQgen_tac list_ss [] 1); |
50 be (XH_to_E ListsXH) 1; |
50 be (XH_to_E ListsXH) 1; |
51 by (EQgen_tac list_ss [] 1); |
51 by (EQgen_tac list_ss [] 1); |
52 by (fast_tac ccl_cs 1); |
52 by (fast_tac ccl_cs 1); |
53 val map_append = result(); |
53 qed "map_append"; |
54 |
54 |
55 (*** Append is associative ***) |
55 (*** Append is associative ***) |
56 |
56 |
57 val prems = goal Stream.thy |
57 val prems = goal Stream.thy |
58 "[| k:Lists(A); l:Lists(A); m:Lists(A) |] ==> k @ l @ m = (k @ l) @ m"; |
58 "[| k:Lists(A); l:Lists(A); m:Lists(A) |] ==> k @ l @ m = (k @ l) @ m"; |
65 be (XH_to_E ListsXH) 1;back(); |
65 be (XH_to_E ListsXH) 1;back(); |
66 by (EQgen_tac list_ss [] 1); |
66 by (EQgen_tac list_ss [] 1); |
67 be (XH_to_E ListsXH) 1; |
67 be (XH_to_E ListsXH) 1; |
68 by (EQgen_tac list_ss [] 1); |
68 by (EQgen_tac list_ss [] 1); |
69 by (fast_tac ccl_cs 1); |
69 by (fast_tac ccl_cs 1); |
70 val append_assoc = result(); |
70 qed "append_assoc"; |
71 |
71 |
72 (*** Appending anything to an infinite list doesn't alter it ****) |
72 (*** Appending anything to an infinite list doesn't alter it ****) |
73 |
73 |
74 val prems = goal Stream.thy "l:ILists(A) ==> l @ m = l"; |
74 val prems = goal Stream.thy "l:ILists(A) ==> l @ m = l"; |
75 by (eq_coinduct3_tac "{p. EX x y.p=<x,y> & (EX l:ILists(A).EX m.x=l@m & y=l)}" 1); |
75 by (eq_coinduct3_tac "{p. EX x y.p=<x,y> & (EX l:ILists(A).EX m.x=l@m & y=l)}" 1); |
76 by (fast_tac (ccl_cs addSIs prems) 1); |
76 by (fast_tac (ccl_cs addSIs prems) 1); |
77 by (safe_tac set_cs); |
77 by (safe_tac set_cs); |
78 be (XH_to_E IListsXH) 1; |
78 be (XH_to_E IListsXH) 1; |
79 by (EQgen_tac list_ss [] 1); |
79 by (EQgen_tac list_ss [] 1); |
80 by (fast_tac ccl_cs 1); |
80 by (fast_tac ccl_cs 1); |
81 val ilist_append = result(); |
81 qed "ilist_append"; |
82 |
82 |
83 (*** The equivalance of two versions of an iteration function ***) |
83 (*** The equivalance of two versions of an iteration function ***) |
84 (* *) |
84 (* *) |
85 (* fun iter1(f,a) = a$iter1(f,f(a)) *) |
85 (* fun iter1(f,a) = a$iter1(f,f(a)) *) |
86 (* fun iter2(f,a) = a$map(f,iter2(f,a)) *) |
86 (* fun iter2(f,a) = a$map(f,iter2(f,a)) *) |
87 |
87 |
88 goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))"; |
88 goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))"; |
89 br (letrecB RS trans) 1; |
89 br (letrecB RS trans) 1; |
90 by (simp_tac term_ss 1); |
90 by (simp_tac term_ss 1); |
91 val iter1B = result(); |
91 qed "iter1B"; |
92 |
92 |
93 goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))"; |
93 goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))"; |
94 br (letrecB RS trans) 1; |
94 br (letrecB RS trans) 1; |
95 br refl 1; |
95 br refl 1; |
96 val iter2B = result(); |
96 qed "iter2B"; |
97 |
97 |
98 val [prem] =goal Stream.thy |
98 val [prem] =goal Stream.thy |
99 "n:Nat ==> map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))"; |
99 "n:Nat ==> map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))"; |
100 br (iter2B RS ssubst) 1;back();back(); |
100 br (iter2B RS ssubst) 1;back();back(); |
101 by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1); |
101 by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1); |
102 val iter2Blemma = result(); |
102 qed "iter2Blemma"; |
103 |
103 |
104 goal Stream.thy "iter1(f,a) = iter2(f,a)"; |
104 goal Stream.thy "iter1(f,a) = iter2(f,a)"; |
105 by (eq_coinduct3_tac |
105 by (eq_coinduct3_tac |
106 "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}" |
106 "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}" |
107 1); |
107 1); |