author  lcp 
Tue, 21 Sep 1993 11:16:19 +0200  
changeset 10  e37080f41102 
parent 0  a5a9c433f639 
child 642  0db578095e6a 
permissions  rwrr 
0  1 
(* Title: 92/CCL/genrec 
2 
ID: $Id$ 

3 
Author: Martin Coen, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
*) 

7 

8 
(*** General Recursive Functions ***) 

9 

10 
val major::prems = goal Wfd.thy 

11 
"[ a : A; \ 

12 
\ !!p g.[ p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) ] ==>\ 

13 
\ h(p,g) : D(p) ] ==> \ 

14 
\ letrec g x be h(x,g) in g(a) : D(a)"; 

15 
br (major RS rev_mp) 1; 

16 
br (wf_wf RS wfd_induct) 1; 

17 
br (letrecB RS ssubst) 1; 

18 
br impI 1; 

19 
bes prems 1; 

20 
br ballI 1; 

21 
be (spec RS mp RS mp) 1; 

22 
by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1)); 

23 
val letrecT = result(); 

24 

25 
goalw Wfd.thy [SPLIT_def] "SPLIT(<a,b>,B) = B(a,b)"; 

26 
br set_ext 1; 

27 
by (fast_tac ccl_cs 1); 

28 
val SPLITB = result(); 

29 

30 
val prems = goalw Wfd.thy [letrec2_def] 

31 
"[ a : A; b : B; \ 

32 
\ !!p q g.[ p:A; q:B; \ 

33 
\ ALL x:A.ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) ] ==>\ 

34 
\ h(p,q,g) : D(p,q) ] ==> \ 

35 
\ letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"; 

36 
br (SPLITB RS subst) 1; 

37 
by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); 

38 
br (SPLITB RS ssubst) 1; 

39 
by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); 

40 
br (SPLITB RS subst) 1; 

41 
by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 

42 
eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); 

43 
val letrec2T = result(); 

44 

45 
goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)"; 

10
e37080f41102
This commit should not have been necessary. For some reason, the previous
lcp
parents:
0
diff
changeset

46 
by (simp_tac (ccl_ss addsimps [SPLITB]) 1); 
0  47 
val lemma = result(); 
48 

49 
val prems = goalw Wfd.thy [letrec3_def] 

50 
"[ a : A; b : B; c : C; \ 

51 
\ !!p q r g.[ p:A; q:B; r:C; \ 

52 
\ ALL x:A.ALL y:B.ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \ 

53 
\ g(x,y,z) : D(x,y,z) ] ==>\ 

54 
\ h(p,q,r,g) : D(p,q,r) ] ==> \ 

55 
\ letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"; 

56 
br (lemma RS subst) 1; 

57 
by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); 

10
e37080f41102
This commit should not have been necessary. For some reason, the previous
lcp
parents:
0
diff
changeset

58 
by (simp_tac (ccl_ss addsimps [SPLITB]) 1); 
0  59 
by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); 
60 
br (lemma RS subst) 1; 

61 
by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 

62 
eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); 

63 
val letrec3T = result(); 

64 

65 
val letrecTs = [letrecT,letrec2T,letrec3T]; 

66 

67 

68 
(*** Type Checking for Recursive Calls ***) 

69 

70 
val major::prems = goal Wfd.thy 

71 
"[ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); \ 

72 
\ g(a) : D(a) ==> g(a) : E; a:A; <a,p>:wf(R) ] ==> \ 

73 
\ g(a) : E"; 

74 
by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1)); 

75 
val rcallT = result(); 

76 

77 
val major::prems = goal Wfd.thy 

78 
"[ ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \ 

79 
\ g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R) ] ==> \ 

80 
\ g(a,b) : E"; 

81 
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1)); 

82 
val rcall2T = result(); 

83 

84 
val major::prems = goal Wfd.thy 

85 
"[ ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \ 

86 
\ g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; \ 

87 
\ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) ] ==> \ 

88 
\ g(a,b,c) : E"; 

89 
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1)); 

90 
val rcall3T = result(); 

91 

92 
val rcallTs = [rcallT,rcall2T,rcall3T]; 

93 

94 
(*** Instantiating an induction hypothesis with an equality assumption ***) 

95 

96 
val prems = goal Wfd.thy 

97 
"[ g(a) = b; ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); \ 

98 
\ [ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); b=g(a); g(a) : D(a) ] ==> P; \ 

99 
\ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A; \ 

100 
\ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R) ] ==> \ 

101 
\ P"; 

102 
brs (prems RL prems) 1; 

103 
brs (prems RL [sym]) 1; 

104 
br rcallT 1; 

105 
by (REPEAT (ares_tac prems 1)); 

106 
val hyprcallT = result(); 

107 

108 
val prems = goal Wfd.thy 

109 
"[ g(a) = b; ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);\ 

110 
\ [ b=g(a); g(a) : D(a) ] ==> P; a:A; <a,p>:wf(R) ] ==> \ 

111 
\ P"; 

112 
brs (prems) 1; 

113 
brs (prems RL [sym]) 1; 

114 
br rcallT 1; 

115 
by (REPEAT (ares_tac prems 1)); 

116 
val hyprcallT = result(); 

117 

118 
val prems = goal Wfd.thy 

119 
"[ g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \ 

120 
\ [ c=g(a,b); g(a,b) : D(a,b) ] ==> P; \ 

121 
\ a:A; b:B; <<a,b>,<p,q>>:wf(R) ] ==> \ 

122 
\ P"; 

123 
brs (prems) 1; 

124 
brs (prems RL [sym]) 1; 

125 
br rcall2T 1; 

126 
by (REPEAT (ares_tac prems 1)); 

127 
val hyprcall2T = result(); 

128 

129 
val prems = goal Wfd.thy 

130 
"[ g(a,b,c) = d; \ 

131 
\ ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \ 

132 
\ [ d=g(a,b,c); g(a,b,c) : D(a,b,c) ] ==> P; \ 

133 
\ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) ] ==> \ 

134 
\ P"; 

135 
brs (prems) 1; 

136 
brs (prems RL [sym]) 1; 

137 
br rcall3T 1; 

138 
by (REPEAT (ares_tac prems 1)); 

139 
val hyprcall3T = result(); 

140 

141 
val hyprcallTs = [hyprcallT,hyprcall2T,hyprcall3T]; 

142 

143 
(*** Rules to Remove Induction Hypotheses after Type Checking ***) 

144 

145 
val prems = goal Wfd.thy 

146 
"[ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P ] ==> \ 

147 
\ P"; 

148 
by (REPEAT (ares_tac prems 1)); 

149 
val rmIH1 = result(); 

150 

151 
val prems = goal Wfd.thy 

152 
"[ ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P ] ==> \ 

153 
\ P"; 

154 
by (REPEAT (ares_tac prems 1)); 

155 
val rmIH2 = result(); 

156 

157 
val prems = goal Wfd.thy 

158 
"[ ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \ 

159 
\ P ] ==> \ 

160 
\ P"; 

161 
by (REPEAT (ares_tac prems 1)); 

162 
val rmIH3 = result(); 

163 

164 
val rmIHs = [rmIH1,rmIH2,rmIH3]; 

165 