author | wenzelm |
Sat, 13 Mar 2010 16:44:12 +0100 | |
changeset 35762 | af3ff2ba4c54 |
parent 27208 | 5fe899199f85 |
child 39159 | 0dec18004e75 |
permissions | -rw-r--r-- |
17456 | 1 |
(* Title: CCL/ex/Stream.thy |
1474 | 2 |
Author: Martin Coen, Cambridge University Computer Laboratory |
0 | 3 |
Copyright 1993 University of Cambridge |
4 |
*) |
|
5 |
||
17456 | 6 |
header {* Programs defined over streams *} |
7 |
||
8 |
theory Stream |
|
9 |
imports List |
|
10 |
begin |
|
0 | 11 |
|
12 |
consts |
|
17456 | 13 |
iter1 :: "[i=>i,i]=>i" |
14 |
iter2 :: "[i=>i,i]=>i" |
|
0 | 15 |
|
17456 | 16 |
defs |
0 | 17 |
|
17456 | 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)" |
|
0 | 20 |
|
20140 | 21 |
|
22 |
(* |
|
23 |
Proving properties about infinite lists using coinduction: |
|
24 |
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. |
|
26 |
*) |
|
27 |
||
28 |
||
29 |
subsection {* Map of composition is composition of maps *} |
|
30 |
||
31 |
lemma map_comp: |
|
32 |
assumes 1: "l:Lists(A)" |
|
33 |
shows "map(f o g,l) = map(f,map(g,l))" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset
|
34 |
apply (tactic {* eq_coinduct3_tac @{context} |
20140 | 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 *}) |
36 |
apply (blast intro: 1) |
|
37 |
apply safe |
|
38 |
apply (drule ListsXH [THEN iffD1]) |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset
|
39 |
apply (tactic "EQgen_tac @{context} [] 1") |
20140 | 40 |
apply fastsimp |
41 |
done |
|
42 |
||
43 |
(*** Mapping the identity function leaves a list unchanged ***) |
|
44 |
||
45 |
lemma map_id: |
|
46 |
assumes 1: "l:Lists(A)" |
|
47 |
shows "map(%x. x,l) = l" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset
|
48 |
apply (tactic {* eq_coinduct3_tac @{context} |
20140 | 49 |
"{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }" 1 *}) |
50 |
apply (blast intro: 1) |
|
51 |
apply safe |
|
52 |
apply (drule ListsXH [THEN iffD1]) |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset
|
53 |
apply (tactic "EQgen_tac @{context} [] 1") |
20140 | 54 |
apply blast |
55 |
done |
|
56 |
||
57 |
||
58 |
subsection {* Mapping distributes over append *} |
|
59 |
||
60 |
lemma map_append: |
|
61 |
assumes "l:Lists(A)" |
|
62 |
and "m:Lists(A)" |
|
63 |
shows "map(f,l@m) = map(f,l) @ map(f,m)" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset
|
64 |
apply (tactic {* eq_coinduct3_tac @{context} |
20140 | 65 |
"{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *}) |
66 |
apply (blast intro: prems) |
|
67 |
apply safe |
|
68 |
apply (drule ListsXH [THEN iffD1]) |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset
|
69 |
apply (tactic "EQgen_tac @{context} [] 1") |
20140 | 70 |
apply (drule ListsXH [THEN iffD1]) |
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset
|
71 |
apply (tactic "EQgen_tac @{context} [] 1") |
20140 | 72 |
apply blast |
73 |
done |
|
74 |
||
75 |
||
76 |
subsection {* Append is associative *} |
|
77 |
||
78 |
lemma append_assoc: |
|
79 |
assumes "k:Lists(A)" |
|
80 |
and "l:Lists(A)" |
|
81 |
and "m:Lists(A)" |
|
82 |
shows "k @ l @ m = (k @ l) @ m" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset
|
83 |
apply (tactic {* eq_coinduct3_tac @{context} |
20140 | 84 |
"{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*}) |
85 |
apply (blast intro: prems) |
|
86 |
apply safe |
|
87 |
apply (drule ListsXH [THEN iffD1]) |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset
|
88 |
apply (tactic "EQgen_tac @{context} [] 1") |
20140 | 89 |
prefer 2 |
90 |
apply blast |
|
91 |
apply (tactic {* DEPTH_SOLVE (etac (XH_to_E (thm "ListsXH")) 1 |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset
|
92 |
THEN EQgen_tac @{context} [] 1) *}) |
20140 | 93 |
done |
94 |
||
95 |
||
96 |
subsection {* Appending anything to an infinite list doesn't alter it *} |
|
97 |
||
98 |
lemma ilist_append: |
|
99 |
assumes "l:ILists(A)" |
|
100 |
shows "l @ m = l" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset
|
101 |
apply (tactic {* eq_coinduct3_tac @{context} |
20140 | 102 |
"{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *}) |
103 |
apply (blast intro: prems) |
|
104 |
apply safe |
|
105 |
apply (drule IListsXH [THEN iffD1]) |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset
|
106 |
apply (tactic "EQgen_tac @{context} [] 1") |
20140 | 107 |
apply blast |
108 |
done |
|
109 |
||
110 |
(*** The equivalance of two versions of an iteration function ***) |
|
111 |
(* *) |
|
112 |
(* fun iter1(f,a) = a$iter1(f,f(a)) *) |
|
113 |
(* fun iter2(f,a) = a$map(f,iter2(f,a)) *) |
|
114 |
||
115 |
lemma iter1B: "iter1(f,a) = a$iter1(f,f(a))" |
|
116 |
apply (unfold iter1_def) |
|
117 |
apply (rule letrecB [THEN trans]) |
|
118 |
apply simp |
|
119 |
done |
|
120 |
||
121 |
lemma iter2B: "iter2(f,a) = a $ map(f,iter2(f,a))" |
|
122 |
apply (unfold iter2_def) |
|
123 |
apply (rule letrecB [THEN trans]) |
|
124 |
apply (rule refl) |
|
125 |
done |
|
126 |
||
127 |
lemma iter2Blemma: |
|
128 |
"n:Nat ==> |
|
129 |
map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))" |
|
130 |
apply (rule_tac P = "%x. ?lhs (x) = ?rhs" in iter2B [THEN ssubst]) |
|
131 |
apply (simp add: nmapBcons) |
|
132 |
done |
|
133 |
||
134 |
lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset
|
135 |
apply (tactic {* eq_coinduct3_tac @{context} |
20140 | 136 |
"{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*}) |
137 |
apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong]) |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset
|
138 |
apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *}) |
20140 | 139 |
apply (subst napply_f, assumption) |
140 |
apply (rule_tac f1 = f in napplyBsucc [THEN subst]) |
|
141 |
apply blast |
|
142 |
done |
|
0 | 143 |
|
144 |
end |