author  lcp 
Mon, 20 Sep 1993 17:02:11 +0200  
changeset 8  c3d2c6dcf3f0 
parent 0  a5a9c433f639 
child 289  78541329ff35 
permissions  rwrr 
0  1 
(* Title: CCL/types 
2 
ID: $Id$ 

3 
Author: Martin Coen, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
For types.thy. 

7 
*) 

8 

9 
open Type; 

10 

11 
val simp_type_defs = [Subtype_def,Unit_def,Bool_def,Plus_def,Sigma_def,Pi_def, 

12 
Lift_def,Tall_def,Tex_def]; 

13 
val ind_type_defs = [Nat_def,List_def]; 

14 

15 
val simp_data_defs = [one_def,inl_def,inr_def]; 

16 
val ind_data_defs = [zero_def,succ_def,nil_def,cons_def]; 

17 

18 
goal Set.thy "A <= B <> (ALL x.x:A > x:B)"; 

19 
by (fast_tac set_cs 1); 

20 
val subsetXH = result(); 

21 

22 
(*** Exhaustion Rules ***) 

23 

24 
fun mk_XH_tac thy defs rls s = prove_goalw thy defs s (fn _ => [cfast_tac rls 1]); 

25 
val XH_tac = mk_XH_tac Type.thy simp_type_defs []; 

26 

27 
val EmptyXH = XH_tac "a : {} <> False"; 

28 
val SubtypeXH = XH_tac "a : {x:A.P(x)} <> (a:A & P(a))"; 

29 
val UnitXH = XH_tac "a : Unit <> a=one"; 

30 
val BoolXH = XH_tac "a : Bool <> a=true  a=false"; 

31 
val PlusXH = XH_tac "a : A+B <> (EX x:A.a=inl(x))  (EX x:B.a=inr(x))"; 

32 
val PiXH = XH_tac "a : PROD x:A.B(x) <> (EX b.a=lam x.b(x) & (ALL x:A.b(x):B(x)))"; 

33 
val SgXH = XH_tac "a : SUM x:A.B(x) <> (EX x:A.EX y:B(x).a=<x,y>)"; 

34 

35 
val XHs = [EmptyXH,SubtypeXH,UnitXH,BoolXH,PlusXH,PiXH,SgXH]; 

36 

37 
val LiftXH = XH_tac "a : [A] <> (a=bot  a:A)"; 

38 
val TallXH = XH_tac "a : TALL X.B(X) <> (ALL X. a:B(X))"; 

39 
val TexXH = XH_tac "a : TEX X.B(X) <> (EX X. a:B(X))"; 

40 

41 
val case_rls = XH_to_Es XHs; 

42 

43 
(*** Canonical Type Rules ***) 

44 

45 
fun mk_canT_tac thy xhs s = prove_goal thy s 

46 
(fn prems => [fast_tac (set_cs addIs (prems @ (xhs RL [iffD2]))) 1]); 

47 
val canT_tac = mk_canT_tac Type.thy XHs; 

48 

49 
val oneT = canT_tac "one : Unit"; 

50 
val trueT = canT_tac "true : Bool"; 

51 
val falseT = canT_tac "false : Bool"; 

52 
val lamT = canT_tac "[ !!x.x:A ==> b(x):B(x) ] ==> lam x.b(x) : Pi(A,B)"; 

53 
val pairT = canT_tac "[ a:A; b:B(a) ] ==> <a,b>:Sigma(A,B)"; 

54 
val inlT = canT_tac "a:A ==> inl(a) : A+B"; 

55 
val inrT = canT_tac "b:B ==> inr(b) : A+B"; 

56 

57 
val canTs = [oneT,trueT,falseT,pairT,lamT,inlT,inrT]; 

58 

59 
(*** NonCanonical Type Rules ***) 

60 

61 
local 

62 
val lemma = prove_goal Type.thy "[ a:B(u); u=v ] ==> a : B(v)" 

63 
(fn prems => [cfast_tac prems 1]); 

64 
in 

65 
fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s 

66 
(fn major::prems => [(resolve_tac ([major] RL top_crls) 1), 

67 
(REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))), 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

68 
(ALLGOALS (asm_simp_tac term_ss)), 
0  69 
(ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' 
70 
eresolve_tac [bspec])), 

71 
(safe_tac (ccl_cs addSIs prems))]); 

72 
end; 

73 

74 
val ncanT_tac = mk_ncanT_tac Type.thy [] case_rls case_rls; 

75 

76 
val ifT = ncanT_tac 

77 
"[ b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) ] ==> \ 

78 
\ if b then t else u : A(b)"; 

79 

80 
val applyT = ncanT_tac 

81 
"[ f : Pi(A,B); a:A ] ==> f ` a : B(a)"; 

82 

83 
val splitT = ncanT_tac 

84 
"[ p:Sigma(A,B); !!x y. [ x:A; y:B(x); p=<x,y> ] ==> c(x,y):C(<x,y>) ] ==> \ 

85 
\ split(p,c):C(p)"; 

86 

87 
val whenT = ncanT_tac 

88 
"[ p:A+B; !!x.[ x:A; p=inl(x) ] ==> a(x):C(inl(x)); \ 

89 
\ !!y.[ y:B; p=inr(y) ] ==> b(y):C(inr(y)) ] ==> \ 

90 
\ when(p,a,b) : C(p)"; 

91 

92 
val ncanTs = [ifT,applyT,splitT,whenT]; 

93 

94 
(*** Subtypes ***) 

95 

96 
val SubtypeD1 = standard ((SubtypeXH RS iffD1) RS conjunct1); 

97 
val SubtypeD2 = standard ((SubtypeXH RS iffD1) RS conjunct2); 

98 

99 
val prems = goal Type.thy 

100 
"[ a:A; P(a) ] ==> a : {x:A. P(x)}"; 

101 
by (REPEAT (resolve_tac (prems@[SubtypeXH RS iffD2,conjI]) 1)); 

102 
val SubtypeI = result(); 

103 

104 
val prems = goal Type.thy 

105 
"[ a : {x:A. P(x)}; [ a:A; P(a) ] ==> Q ] ==> Q"; 

106 
by (REPEAT (resolve_tac (prems@[SubtypeD1,SubtypeD2]) 1)); 

107 
val SubtypeE = result(); 

108 

109 
(*** Monotonicity ***) 

110 

111 
goal Type.thy "mono (%X.X)"; 

112 
by (REPEAT (ares_tac [monoI] 1)); 

113 
val idM = result(); 

114 

115 
goal Type.thy "mono(%X.A)"; 

116 
by (REPEAT (ares_tac [monoI,subset_refl] 1)); 

117 
val constM = result(); 

118 

119 
val major::prems = goal Type.thy 

120 
"mono(%X.A(X)) ==> mono(%X.[A(X)])"; 

121 
br (subsetI RS monoI) 1; 

122 
bd (LiftXH RS iffD1) 1; 

123 
be disjE 1; 

124 
be (disjI1 RS (LiftXH RS iffD2)) 1; 

125 
br (disjI2 RS (LiftXH RS iffD2)) 1; 

126 
be (major RS monoD RS subsetD) 1; 

127 
ba 1; 

128 
val LiftM = result(); 

129 

130 
val prems = goal Type.thy 

131 
"[ mono(%X.A(X)); !!x X. x:A(X) ==> mono(%X.B(X,x)) ] ==> \ 

132 
\ mono(%X.Sigma(A(X),B(X)))"; 

133 
by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE 

134 
eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE 

135 
(resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE 

136 
hyp_subst_tac 1)); 

137 
val SgM = result(); 

138 

139 
val prems = goal Type.thy 

140 
"[ !!x. x:A ==> mono(%X.B(X,x)) ] ==> mono(%X.Pi(A,B(X)))"; 

141 
by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE 

142 
eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE 

143 
(resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE 

144 
hyp_subst_tac 1)); 

145 
val PiM = result(); 

146 

147 
val prems = goal Type.thy 

148 
"[ mono(%X.A(X)); mono(%X.B(X)) ] ==> mono(%X.A(X)+B(X))"; 

149 
by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE 

150 
eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE 

151 
(resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE 

152 
hyp_subst_tac 1)); 

153 
val PlusM = result(); 

154 

155 
(**************** RECURSIVE TYPES ******************) 

156 

157 
(*** Conversion Rules for Fixed Points via monotonicity and Tarski ***) 

158 

159 
goal Type.thy "mono(%X.Unit+X)"; 

160 
by (REPEAT (ares_tac [PlusM,constM,idM] 1)); 

161 
val NatM = result(); 

162 
val def_NatB = result() RS (Nat_def RS def_lfp_Tarski); 

163 

164 
goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))"; 

165 
by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1)); 

166 
val ListM = result(); 

167 
val def_ListB = result() RS (List_def RS def_lfp_Tarski); 

168 
val def_ListsB = result() RS (Lists_def RS def_gfp_Tarski); 

169 

170 
goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))"; 

171 
by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1)); 

172 
val IListsM = result(); 

173 
val def_IListsB = result() RS (ILists_def RS def_gfp_Tarski); 

174 

175 
val ind_type_eqs = [def_NatB,def_ListB,def_ListsB,def_IListsB]; 

176 

177 
(*** Exhaustion Rules ***) 

178 

179 
fun mk_iXH_tac teqs ddefs rls s = prove_goalw Type.thy ddefs s 

180 
(fn _ => [resolve_tac (teqs RL [XHlemma1]) 1, 

181 
fast_tac (set_cs addSIs canTs addSEs case_rls) 1]); 

182 

183 
val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs []; 

184 

185 
val NatXH = iXH_tac "a : Nat <> (a=zero  (EX x:Nat.a=succ(x)))"; 

186 
val ListXH = iXH_tac "a : List(A) <> (a=[]  (EX x:A.EX xs:List(A).a=x.xs))"; 

187 
val ListsXH = iXH_tac "a : Lists(A) <> (a=[]  (EX x:A.EX xs:Lists(A).a=x.xs))"; 

188 
val IListsXH = iXH_tac "a : ILists(A) <> (EX x:A.EX xs:ILists(A).a=x.xs)"; 

189 

190 
val iXHs = [NatXH,ListXH]; 

191 
val icase_rls = XH_to_Es iXHs; 

192 

193 
(*** Type Rules ***) 

194 

195 
val icanT_tac = mk_canT_tac Type.thy iXHs; 

196 
val incanT_tac = mk_ncanT_tac Type.thy [] icase_rls case_rls; 

197 

198 
val zeroT = icanT_tac "zero : Nat"; 

199 
val succT = icanT_tac "n:Nat ==> succ(n) : Nat"; 

200 
val nilT = icanT_tac "[] : List(A)"; 

201 
val consT = icanT_tac "[ h:A; t:List(A) ] ==> h.t : List(A)"; 

202 

203 
val icanTs = [zeroT,succT,nilT,consT]; 

204 

205 
val ncaseT = incanT_tac 

206 
"[ n:Nat; n=zero ==> b:C(zero); \ 

207 
\ !!x.[ x:Nat; n=succ(x) ] ==> c(x):C(succ(x)) ] ==> \ 

208 
\ ncase(n,b,c) : C(n)"; 

209 

210 
val lcaseT = incanT_tac 

211 
"[ l:List(A); l=[] ==> b:C([]); \ 

212 
\ !!h t.[ h:A; t:List(A); l=h.t ] ==> c(h,t):C(h.t) ] ==> \ 

213 
\ lcase(l,b,c) : C(l)"; 

214 

215 
val incanTs = [ncaseT,lcaseT]; 

216 

217 
(*** Induction Rules ***) 

218 

219 
val ind_Ms = [NatM,ListM]; 

220 

221 
fun mk_ind_tac ddefs tdefs Ms canTs case_rls s = prove_goalw Type.thy ddefs s 

222 
(fn major::prems => [resolve_tac (Ms RL ([major] RL (tdefs RL [def_induct]))) 1, 

223 
fast_tac (set_cs addSIs (prems @ canTs) addSEs case_rls) 1]); 

224 

225 
val ind_tac = mk_ind_tac ind_data_defs ind_type_defs ind_Ms canTs case_rls; 

226 

227 
val Nat_ind = ind_tac 

228 
"[ n:Nat; P(zero); !!x.[ x:Nat; P(x) ] ==> P(succ(x)) ] ==> \ 

229 
\ P(n)"; 

230 

231 
val List_ind = ind_tac 

232 
"[ l:List(A); P([]); \ 

233 
\ !!x xs.[ x:A; xs:List(A); P(xs) ] ==> P(x.xs) ] ==> \ 

234 
\ P(l)"; 

235 

236 
val inds = [Nat_ind,List_ind]; 

237 

238 
(*** Primitive Recursive Rules ***) 

239 

240 
fun mk_prec_tac inds s = prove_goal Type.thy s 

241 
(fn major::prems => [resolve_tac ([major] RL inds) 1, 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

242 
ALLGOALS (simp_tac term_ss THEN' 
0  243 
fast_tac (set_cs addSIs prems))]); 
244 
val prec_tac = mk_prec_tac inds; 

245 

246 
val nrecT = prec_tac 

247 
"[ n:Nat; b:C(zero); \ 

248 
\ !!x g.[ x:Nat; g:C(x) ] ==> c(x,g):C(succ(x)) ] ==> \ 

249 
\ nrec(n,b,c) : C(n)"; 

250 

251 
val lrecT = prec_tac 

252 
"[ l:List(A); b:C([]); \ 

253 
\ !!x xs g.[ x:A; xs:List(A); g:C(xs) ] ==> c(x,xs,g):C(x.xs) ] ==> \ 

254 
\ lrec(l,b,c) : C(l)"; 

255 

256 
val precTs = [nrecT,lrecT]; 

257 

258 

259 
(*** Theorem proving ***) 

260 

261 
val [major,minor] = goal Type.thy 

262 
"[ <a,b> : Sigma(A,B); [ a:A; b:B(a) ] ==> P \ 

263 
\ ] ==> P"; 

264 
br (major RS (XH_to_E SgXH)) 1; 

265 
br minor 1; 

266 
by (ALLGOALS (fast_tac term_cs)); 

267 
val SgE2 = result(); 

268 

269 
(* General theorem proving ignores noncanonical termformers, *) 

270 
(*  intro rules are type rules for canonical terms *) 

271 
(*  elim rules are case rules (no noncanonical terms appear) *) 

272 

273 
val type_cs = term_cs addSIs (SubtypeI::(canTs @ icanTs)) 

274 
addSEs (SubtypeE::(XH_to_Es XHs)); 

275 

276 

277 
(*** Infinite Data Types ***) 

278 

279 
val [mono] = goal Type.thy "mono(f) ==> lfp(f) <= gfp(f)"; 

280 
br (lfp_lowerbound RS subset_trans) 1; 

281 
br (mono RS gfp_lemma3) 1; 

282 
br subset_refl 1; 

283 
val lfp_subset_gfp = result(); 

284 

285 
val prems = goal Type.thy 

286 
"[ a:A; !!x X.[ x:A; ALL y:A.t(y):X ] ==> t(x) : B(X) ] ==> \ 

287 
\ t(a) : gfp(B)"; 

288 
br coinduct 1; 

289 
by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1); 

290 
by (ALLGOALS (fast_tac (ccl_cs addSIs prems))); 

291 
val gfpI = result(); 

292 

293 
val rew::prem::prems = goal Type.thy 

294 
"[ C==gfp(B); a:A; !!x X.[ x:A; ALL y:A.t(y):X ] ==> t(x) : B(X) ] ==> \ 

295 
\ t(a) : C"; 

296 
by (rewtac rew); 

297 
by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1)); 

298 
val def_gfpI = result(); 

299 

300 
(* EG *) 

301 

302 
val prems = goal Type.thy 

303 
"letrec g x be zero.g(x) in g(bot) : Lists(Nat)"; 

304 
by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1); 

305 
br (letrecB RS ssubst) 1; 

306 
bw cons_def; 

307 
by (fast_tac type_cs 1); 

308 
result(); 