author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 47966  b8a94ed1646e 
child 58889  5b7a9633cfa8 
permissions  rwrr 
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 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
41526
diff
changeset

12 
definition iter1 :: "[i=>i,i]=>i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
41526
diff
changeset

13 
where "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)" 
0  14 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
41526
diff
changeset

15 
definition iter2 :: "[i=>i,i]=>i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
41526
diff
changeset

16 
where "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)" 
20140  17 

18 
(* 

19 
Proving properties about infinite lists using coinduction: 

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

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

22 
*) 

23 

24 

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

26 

27 
lemma map_comp: 

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

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
41526
diff
changeset

29 
shows "map(f \<circ> g,l) = map(f,map(g,l))" 
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset

30 
apply (tactic {* eq_coinduct3_tac @{context} 
42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
41526
diff
changeset

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 *}) 
20140  32 
apply (blast intro: 1) 
33 
apply safe 

34 
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

35 
apply (tactic "EQgen_tac @{context} [] 1") 
47966  36 
apply fastforce 
20140  37 
done 
38 

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

40 

41 
lemma map_id: 

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

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

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

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

47 
apply safe 

48 
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

49 
apply (tactic "EQgen_tac @{context} [] 1") 
20140  50 
apply blast 
51 
done 

52 

53 

54 
subsection {* Mapping distributes over append *} 

55 

56 
lemma map_append: 

57 
assumes "l:Lists(A)" 

58 
and "m:Lists(A)" 

59 
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

60 
apply (tactic {* eq_coinduct3_tac @{context} 
20140  61 
"{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 *}) 
41526  62 
apply (blast intro: assms) 
20140  63 
apply safe 
64 
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

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

67 
apply (tactic "EQgen_tac @{context} [] 1") 
20140  68 
apply blast 
69 
done 

70 

71 

72 
subsection {* Append is associative *} 

73 

74 
lemma append_assoc: 

75 
assumes "k:Lists(A)" 

76 
and "l:Lists(A)" 

77 
and "m:Lists(A)" 

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

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

79 
apply (tactic {* eq_coinduct3_tac @{context} 
20140  80 
"{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*}) 
41526  81 
apply (blast intro: assms) 
20140  82 
apply safe 
83 
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

84 
apply (tactic "EQgen_tac @{context} [] 1") 
20140  85 
prefer 2 
86 
apply blast 

39159  87 
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

88 
THEN EQgen_tac @{context} [] 1) *}) 
20140  89 
done 
90 

91 

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

93 

94 
lemma ilist_append: 

95 
assumes "l:ILists(A)" 

96 
shows "l @ m = l" 

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

97 
apply (tactic {* eq_coinduct3_tac @{context} 
20140  98 
"{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *}) 
41526  99 
apply (blast intro: assms) 
20140  100 
apply safe 
101 
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

102 
apply (tactic "EQgen_tac @{context} [] 1") 
20140  103 
apply blast 
104 
done 

105 

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

107 
(* *) 

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

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

110 

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

112 
apply (unfold iter1_def) 

113 
apply (rule letrecB [THEN trans]) 

114 
apply simp 

115 
done 

116 

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

118 
apply (unfold iter2_def) 

119 
apply (rule letrecB [THEN trans]) 

120 
apply (rule refl) 

121 
done 

122 

123 
lemma iter2Blemma: 

124 
"n:Nat ==> 

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

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

127 
apply (simp add: nmapBcons) 

128 
done 

129 

130 
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

131 
apply (tactic {* eq_coinduct3_tac @{context} 
20140  132 
"{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*}) 
133 
apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong]) 

39159  134 
apply (tactic {* EQgen_tac @{context} [@{thm iter1B}, @{thm iter2Blemma}] 1 *}) 
20140  135 
apply (subst napply_f, assumption) 
136 
apply (rule_tac f1 = f in napplyBsucc [THEN subst]) 

137 
apply blast 

138 
done 

0  139 

140 
end 