equal
deleted
inserted
replaced
7 |
7 |
8 theory Stream |
8 theory Stream |
9 imports List |
9 imports List |
10 begin |
10 begin |
11 |
11 |
12 consts |
12 definition iter1 :: "[i=>i,i]=>i" |
13 iter1 :: "[i=>i,i]=>i" |
13 where "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)" |
14 iter2 :: "[i=>i,i]=>i" |
|
15 |
14 |
16 defs |
15 definition iter2 :: "[i=>i,i]=>i" |
17 |
16 where "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)" |
18 iter1_def: "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)" |
|
19 iter2_def: "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)" |
|
20 |
|
21 |
17 |
22 (* |
18 (* |
23 Proving properties about infinite lists using coinduction: |
19 Proving properties about infinite lists using coinduction: |
24 Lists(A) is the set of all finite and infinite lists of elements of A. |
20 Lists(A) is the set of all finite and infinite lists of elements of A. |
25 ILists(A) is the set of infinite lists of elements of A. |
21 ILists(A) is the set of infinite lists of elements of A. |
28 |
24 |
29 subsection {* Map of composition is composition of maps *} |
25 subsection {* Map of composition is composition of maps *} |
30 |
26 |
31 lemma map_comp: |
27 lemma map_comp: |
32 assumes 1: "l:Lists(A)" |
28 assumes 1: "l:Lists(A)" |
33 shows "map(f o g,l) = map(f,map(g,l))" |
29 shows "map(f \<circ> g,l) = map(f,map(g,l))" |
34 apply (tactic {* eq_coinduct3_tac @{context} |
30 apply (tactic {* eq_coinduct3_tac @{context} |
35 "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f o g,l) & y=map (f,map (g,l)))}" 1 *}) |
31 "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f \<circ> g,l) & y=map (f,map (g,l)))}" 1 *}) |
36 apply (blast intro: 1) |
32 apply (blast intro: 1) |
37 apply safe |
33 apply safe |
38 apply (drule ListsXH [THEN iffD1]) |
34 apply (drule ListsXH [THEN iffD1]) |
39 apply (tactic "EQgen_tac @{context} [] 1") |
35 apply (tactic "EQgen_tac @{context} [] 1") |
40 apply fastsimp |
36 apply fastsimp |