author  wenzelm 
Sun, 30 Nov 2008 14:43:29 +0100  
changeset 28917  20f43e0e0958 
parent 27208  5fe899199f85 
child 35762  af3ff2ba4c54 
permissions  rwrr 
17456  1 
(* Title: CCL/ex/Stream.thy 
0  2 
ID: $Id$ 
1474  3 
Author: Martin Coen, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 
*) 

6 

17456  7 
header {* Programs defined over streams *} 
8 

9 
theory Stream 

10 
imports List 

11 
begin 

0  12 

13 
consts 

17456  14 
iter1 :: "[i=>i,i]=>i" 
15 
iter2 :: "[i=>i,i]=>i" 

0  16 

17456  17 
defs 
0  18 

17456  19 
iter1_def: "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)" 
20 
iter2_def: "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)" 

0  21 

20140  22 

23 
(* 

24 
Proving properties about infinite lists using coinduction: 

25 
Lists(A) is the set of all finite and infinite lists of elements of A. 

26 
ILists(A) is the set of infinite lists of elements of A. 

27 
*) 

28 

29 

30 
subsection {* Map of composition is composition of maps *} 

31 

32 
lemma map_comp: 

33 
assumes 1: "l:Lists(A)" 

34 
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

35 
apply (tactic {* eq_coinduct3_tac @{context} 
20140  36 
"{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f o g,l) & y=map (f,map (g,l)))}" 1 *}) 
37 
apply (blast intro: 1) 

38 
apply safe 

39 
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

40 
apply (tactic "EQgen_tac @{context} [] 1") 
20140  41 
apply fastsimp 
42 
done 

43 

44 
(*** Mapping the identity function leaves a list unchanged ***) 

45 

46 
lemma map_id: 

47 
assumes 1: "l:Lists(A)" 

48 
shows "map(%x. x,l) = l" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset

49 
apply (tactic {* eq_coinduct3_tac @{context} 
20140  50 
"{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }" 1 *}) 
51 
apply (blast intro: 1) 

52 
apply safe 

53 
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

54 
apply (tactic "EQgen_tac @{context} [] 1") 
20140  55 
apply blast 
56 
done 

57 

58 

59 
subsection {* Mapping distributes over append *} 

60 

61 
lemma map_append: 

62 
assumes "l:Lists(A)" 

63 
and "m:Lists(A)" 

64 
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

65 
apply (tactic {* eq_coinduct3_tac @{context} 
20140  66 
"{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 *}) 
67 
apply (blast intro: prems) 

68 
apply safe 

69 
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

70 
apply (tactic "EQgen_tac @{context} [] 1") 
20140  71 
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

72 
apply (tactic "EQgen_tac @{context} [] 1") 
20140  73 
apply blast 
74 
done 

75 

76 

77 
subsection {* Append is associative *} 

78 

79 
lemma append_assoc: 

80 
assumes "k:Lists(A)" 

81 
and "l:Lists(A)" 

82 
and "m:Lists(A)" 

83 
shows "k @ l @ m = (k @ l) @ m" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset

84 
apply (tactic {* eq_coinduct3_tac @{context} 
20140  85 
"{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*}) 
86 
apply (blast intro: prems) 

87 
apply safe 

88 
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

89 
apply (tactic "EQgen_tac @{context} [] 1") 
20140  90 
prefer 2 
91 
apply blast 

92 
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

93 
THEN EQgen_tac @{context} [] 1) *}) 
20140  94 
done 
95 

96 

97 
subsection {* Appending anything to an infinite list doesn't alter it *} 

98 

99 
lemma ilist_append: 

100 
assumes "l:ILists(A)" 

101 
shows "l @ m = l" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset

102 
apply (tactic {* eq_coinduct3_tac @{context} 
20140  103 
"{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *}) 
104 
apply (blast intro: prems) 

105 
apply safe 

106 
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

107 
apply (tactic "EQgen_tac @{context} [] 1") 
20140  108 
apply blast 
109 
done 

110 

111 
(*** The equivalance of two versions of an iteration function ***) 

112 
(* *) 

113 
(* fun iter1(f,a) = a$iter1(f,f(a)) *) 

114 
(* fun iter2(f,a) = a$map(f,iter2(f,a)) *) 

115 

116 
lemma iter1B: "iter1(f,a) = a$iter1(f,f(a))" 

117 
apply (unfold iter1_def) 

118 
apply (rule letrecB [THEN trans]) 

119 
apply simp 

120 
done 

121 

122 
lemma iter2B: "iter2(f,a) = a $ map(f,iter2(f,a))" 

123 
apply (unfold iter2_def) 

124 
apply (rule letrecB [THEN trans]) 

125 
apply (rule refl) 

126 
done 

127 

128 
lemma iter2Blemma: 

129 
"n:Nat ==> 

130 
map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))" 

131 
apply (rule_tac P = "%x. ?lhs (x) = ?rhs" in iter2B [THEN ssubst]) 

132 
apply (simp add: nmapBcons) 

133 
done 

134 

135 
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

136 
apply (tactic {* eq_coinduct3_tac @{context} 
20140  137 
"{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*}) 
138 
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

139 
apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *}) 
20140  140 
apply (subst napply_f, assumption) 
141 
apply (rule_tac f1 = f in napplyBsucc [THEN subst]) 

142 
apply blast 

143 
done 

0  144 

145 
end 