author  wenzelm 
Mon, 09 Oct 2006 02:20:10 +0200  
changeset 20917  803c94363ccc 
parent 20140  98acc6d0fab6 
child 24790  3be1580de4cc 
permissions  rwrr 
17456  1 
(* Title: CCL/Term.thy 
0  2 
ID: $Id$ 
1474  3 
Author: Martin Coen 
0  4 
Copyright 1993 University of Cambridge 
5 
*) 

6 

17456  7 
header {* Definitions of usual program constructs in CCL *} 
8 

9 
theory Term 

10 
imports CCL 

11 
begin 

0  12 

13 
consts 

14 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

15 
one :: "i" 
0  16 

19796  17 
"if" :: "[i,i,i]=>i" ("(3if _/ then _/ else _)" [0,0,60] 60) 
0  18 

17456  19 
inl :: "i=>i" 
20 
inr :: "i=>i" 

21 
when :: "[i,i=>i,i=>i]=>i" 

0  22 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

23 
split :: "[i,[i,i]=>i]=>i" 
17456  24 
fst :: "i=>i" 
25 
snd :: "i=>i" 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

26 
thd :: "i=>i" 
0  27 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

28 
zero :: "i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

29 
succ :: "i=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

30 
ncase :: "[i,i,i=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

31 
nrec :: "[i,i,[i,i]=>i]=>i" 
0  32 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

33 
nil :: "i" ("([])") 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

34 
"$" :: "[i,i]=>i" (infixr 80) 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

35 
lcase :: "[i,i,[i,i]=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

36 
lrec :: "[i,i,[i,i,i]=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

37 

17456  38 
"let" :: "[i,i=>i]=>i" 
998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

39 
letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

40 
letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" 
17456  41 
letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" 
0  42 

14765  43 
syntax 
998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

44 
"@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" 
1474  45 
[0,0,60] 60) 
998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

46 

91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

47 
"@letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)" 
1474  48 
[0,0,0,60] 60) 
0  49 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

50 
"@letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" 
1474  51 
[0,0,0,0,60] 60) 
0  52 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

53 
"@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" 
1474  54 
[0,0,0,0,0,60] 60) 
998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

55 

17456  56 
ML {* 
0  57 
(** Quantifier translations: variable binding **) 
58 

17781  59 
(* FIXME does not handle "_idtdummy" *) 
2709  60 
(* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *) 
61 

0  62 
fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b); 
63 
fun let_tr' [a,Abs(id,T,b)] = 

64 
let val (id',b') = variant_abs(id,T,b) 

65 
in Const("@let",dummyT) $ Free(id',T) $ a $ b' end; 

66 

17456  67 
fun letrec_tr [Free(f,S),Free(x,T),a,b] = 
0  68 
Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b); 
17456  69 
fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] = 
0  70 
Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b); 
17456  71 
fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] = 
0  72 
Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b); 
73 

74 
fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] = 

75 
let val (f',b') = variant_abs(ff,SS,b) 

76 
val (_,a'') = variant_abs(f,S,a) 

77 
val (x',a') = variant_abs(x,T,a'') 

78 
in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end; 

79 
fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] = 

80 
let val (f',b') = variant_abs(ff,SS,b) 

81 
val ( _,a1) = variant_abs(f,S,a) 

82 
val (y',a2) = variant_abs(y,U,a1) 

83 
val (x',a') = variant_abs(x,T,a2) 

84 
in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b' 

85 
end; 

86 
fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] = 

87 
let val (f',b') = variant_abs(ff,SS,b) 

88 
val ( _,a1) = variant_abs(f,S,a) 

89 
val (z',a2) = variant_abs(z,V,a1) 

90 
val (y',a3) = variant_abs(y,U,a2) 

91 
val (x',a') = variant_abs(x,T,a3) 

92 
in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b' 

93 
end; 

94 

17456  95 
*} 
96 

97 
parse_translation {* 

98 
[("@let", let_tr), 

99 
("@letrec", letrec_tr), 

100 
("@letrec2", letrec2_tr), 

101 
("@letrec3", letrec3_tr)] *} 

102 

103 
print_translation {* 

104 
[("let", let_tr'), 

105 
("letrec", letrec_tr'), 

106 
("letrec2", letrec2_tr'), 

107 
("letrec3", letrec3_tr')] *} 

108 

109 
consts 

110 
napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) 

111 

112 
axioms 

113 

114 
one_def: "one == true" 

115 
if_def: "if b then t else u == case(b,t,u,% x y. bot,%v. bot)" 

116 
inl_def: "inl(a) == <true,a>" 

117 
inr_def: "inr(b) == <false,b>" 

118 
when_def: "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))" 

119 
split_def: "split(t,f) == case(t,bot,bot,f,%u. bot)" 

120 
fst_def: "fst(t) == split(t,%x y. x)" 

121 
snd_def: "snd(t) == split(t,%x y. y)" 

122 
thd_def: "thd(t) == split(t,%x p. split(p,%y z. z))" 

123 
zero_def: "zero == inl(one)" 

124 
succ_def: "succ(n) == inr(n)" 

125 
ncase_def: "ncase(n,b,c) == when(n,%x. b,%y. c(y))" 

126 
nrec_def: " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)" 

127 
nil_def: "[] == inl(one)" 

128 
cons_def: "h$t == inr(<h,t>)" 

129 
lcase_def: "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))" 

130 
lrec_def: "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)" 

131 

132 
let_def: "let x be t in f(x) == case(t,f(true),f(false),%x y. f(<x,y>),%u. f(lam x. u(x)))" 

133 
letrec_def: 

134 
"letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)" 

135 

136 
letrec2_def: "letrec g x y be h(x,y,g) in f(g)== 

137 
letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>))) 

138 
in f(%x y. g'(<x,y>))" 

139 

140 
letrec3_def: "letrec g x y z be h(x,y,z,g) in f(g) == 

141 
letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>)))) 

142 
in f(%x y z. g'(<x,<y,z>>))" 

143 

144 
napply_def: "f ^n` a == nrec(n,a,%x g. f(g))" 

145 

20140  146 

147 
lemmas simp_can_defs = one_def inl_def inr_def 

148 
and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def 

149 
lemmas simp_defs = simp_can_defs simp_ncan_defs 

150 

151 
lemmas ind_can_defs = zero_def succ_def nil_def cons_def 

152 
and ind_ncan_defs = ncase_def nrec_def lcase_def lrec_def 

153 
lemmas ind_defs = ind_can_defs ind_ncan_defs 

154 

155 
lemmas data_defs = simp_defs ind_defs napply_def 

156 
and genrec_defs = letrec_def letrec2_def letrec3_def 

157 

158 

159 
subsection {* Beta Rules, including strictness *} 

160 

161 
lemma letB: "~ t=bot ==> let x be t in f(x) = f(t)" 

162 
apply (unfold let_def) 

163 
apply (erule rev_mp) 

164 
apply (rule_tac t = "t" in term_case) 

165 
apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam) 

166 
done 

167 

168 
lemma letBabot: "let x be bot in f(x) = bot" 

169 
apply (unfold let_def) 

170 
apply (rule caseBbot) 

171 
done 

172 

173 
lemma letBbbot: "let x be t in bot = bot" 

174 
apply (unfold let_def) 

175 
apply (rule_tac t = t in term_case) 

176 
apply (rule caseBbot) 

177 
apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam) 

178 
done 

179 

180 
lemma applyB: "(lam x. b(x)) ` a = b(a)" 

181 
apply (unfold apply_def) 

182 
apply (simp add: caseBtrue caseBfalse caseBpair caseBlam) 

183 
done 

184 

185 
lemma applyBbot: "bot ` a = bot" 

186 
apply (unfold apply_def) 

187 
apply (rule caseBbot) 

188 
done 

189 

190 
lemma fixB: "fix(f) = f(fix(f))" 

191 
apply (unfold fix_def) 

192 
apply (rule applyB [THEN ssubst], rule refl) 

193 
done 

194 

195 
lemma letrecB: 

196 
"letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))" 

197 
apply (unfold letrec_def) 

198 
apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl) 

199 
done 

200 

201 
lemmas rawBs = caseBs applyB applyBbot 

202 

203 
ML {* 

204 
local 

205 
val letrecB = thm "letrecB" 

206 
val rawBs = thms "rawBs" 

207 
val data_defs = thms "data_defs" 

208 
in 

209 

210 
fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s 

211 
(fn _ => [stac letrecB 1, 

212 
simp_tac (simpset () addsimps rawBs) 1]); 

213 
fun mk_beta_rl s = raw_mk_beta_rl data_defs s; 

214 

215 
fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s 

216 
(fn _ => [simp_tac (simpset () addsimps rawBs 

217 
setloop (stac letrecB)) 1]); 

218 
fun mk_beta_rl s = raw_mk_beta_rl data_defs s; 

17456  219 

220 
end 

20140  221 
*} 
222 

223 
ML {* 

224 
bind_thm ("ifBtrue", mk_beta_rl "if true then t else u = t"); 

225 
bind_thm ("ifBfalse", mk_beta_rl "if false then t else u = u"); 

226 
bind_thm ("ifBbot", mk_beta_rl "if bot then t else u = bot"); 

227 

228 
bind_thm ("whenBinl", mk_beta_rl "when(inl(a),t,u) = t(a)"); 

229 
bind_thm ("whenBinr", mk_beta_rl "when(inr(a),t,u) = u(a)"); 

230 
bind_thm ("whenBbot", mk_beta_rl "when(bot,t,u) = bot"); 

231 

232 
bind_thm ("splitB", mk_beta_rl "split(<a,b>,h) = h(a,b)"); 

233 
bind_thm ("splitBbot", mk_beta_rl "split(bot,h) = bot"); 

234 
bind_thm ("fstB", mk_beta_rl "fst(<a,b>) = a"); 

235 
bind_thm ("fstBbot", mk_beta_rl "fst(bot) = bot"); 

236 
bind_thm ("sndB", mk_beta_rl "snd(<a,b>) = b"); 

237 
bind_thm ("sndBbot", mk_beta_rl "snd(bot) = bot"); 

238 
bind_thm ("thdB", mk_beta_rl "thd(<a,<b,c>>) = c"); 

239 
bind_thm ("thdBbot", mk_beta_rl "thd(bot) = bot"); 

240 

241 
bind_thm ("ncaseBzero", mk_beta_rl "ncase(zero,t,u) = t"); 

242 
bind_thm ("ncaseBsucc", mk_beta_rl "ncase(succ(n),t,u) = u(n)"); 

243 
bind_thm ("ncaseBbot", mk_beta_rl "ncase(bot,t,u) = bot"); 

244 
bind_thm ("nrecBzero", mk_beta_rl "nrec(zero,t,u) = t"); 

245 
bind_thm ("nrecBsucc", mk_beta_rl "nrec(succ(n),t,u) = u(n,nrec(n,t,u))"); 

246 
bind_thm ("nrecBbot", mk_beta_rl "nrec(bot,t,u) = bot"); 

247 

248 
bind_thm ("lcaseBnil", mk_beta_rl "lcase([],t,u) = t"); 

249 
bind_thm ("lcaseBcons", mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)"); 

250 
bind_thm ("lcaseBbot", mk_beta_rl "lcase(bot,t,u) = bot"); 

251 
bind_thm ("lrecBnil", mk_beta_rl "lrec([],t,u) = t"); 

252 
bind_thm ("lrecBcons", mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))"); 

253 
bind_thm ("lrecBbot", mk_beta_rl "lrec(bot,t,u) = bot"); 

254 

255 
bind_thm ("letrec2B", raw_mk_beta_rl (thms "data_defs" @ [thm "letrec2_def"]) 

256 
"letrec g x y be h(x,y,g) in g(p,q) = h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))"); 

257 

258 
bind_thm ("letrec3B", raw_mk_beta_rl (thms "data_defs" @ [thm "letrec3_def"]) 

259 
"letrec g x y z be h(x,y,z,g) in g(p,q,r) = h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))"); 

260 

261 
bind_thm ("napplyBzero", mk_beta_rl "f^zero`a = a"); 

262 
bind_thm ("napplyBsucc", mk_beta_rl "f^succ(n)`a = f(f^n`a)"); 

263 

264 
bind_thms ("termBs", [thm "letB", thm "applyB", thm "applyBbot", splitB,splitBbot, 

265 
fstB,fstBbot,sndB,sndBbot,thdB,thdBbot, 

266 
ifBtrue,ifBfalse,ifBbot,whenBinl,whenBinr,whenBbot, 

267 
ncaseBzero,ncaseBsucc,ncaseBbot,nrecBzero,nrecBsucc,nrecBbot, 

268 
lcaseBnil,lcaseBcons,lcaseBbot,lrecBnil,lrecBcons,lrecBbot, 

269 
napplyBzero,napplyBsucc]); 

270 
*} 

271 

272 

273 
subsection {* Constructors are injective *} 

274 

275 
ML {* 

276 

277 
bind_thms ("term_injs", map (mk_inj_rl (the_context ()) 

278 
[thm "applyB", thm "splitB", thm "whenBinl", thm "whenBinr", thm "ncaseBsucc", thm "lcaseBcons"]) 

279 
["(inl(a) = inl(a')) <> (a=a')", 

280 
"(inr(a) = inr(a')) <> (a=a')", 

281 
"(succ(a) = succ(a')) <> (a=a')", 

282 
"(a$b = a'$b') <> (a=a' & b=b')"]) 

283 
*} 

284 

285 

286 
subsection {* Constructors are distinct *} 

287 

288 
ML {* 

289 
bind_thms ("term_dstncts", 

290 
mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs") 

291 
[["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","op $"]]); 

292 
*} 

293 

294 

295 
subsection {* Rules for preorder @{text "[="} *} 

296 

297 
ML {* 

298 

299 
local 

300 
fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ => 

301 
[simp_tac (simpset () addsimps (thms "ccl_porews")) 1]) 

302 
in 

303 
val term_porews = map mk_thm ["inl(a) [= inl(a') <> a [= a'", 

304 
"inr(b) [= inr(b') <> b [= b'", 

305 
"succ(n) [= succ(n') <> n [= n'", 

306 
"x$xs [= x'$xs' <> x [= x' & xs [= xs'"] 

307 
end; 

308 

309 
bind_thms ("term_porews", term_porews); 

310 
*} 

311 

312 
subsection {* Rewriting and Proving *} 

313 

314 
ML {* 

315 
bind_thms ("term_injDs", XH_to_Ds term_injs); 

316 
*} 

317 

20917  318 
lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews 
319 

20140  320 
lemmas [simp] = term_rews 
20917  321 
lemmas [elim!] = term_dstncts [THEN notE] 
322 
lemmas [dest!] = term_injDs 

20140  323 

324 
end 