--- a/src/CCL/Term.thy Sat Sep 17 14:02:31 2005 +0200
+++ b/src/CCL/Term.thy Sat Sep 17 17:35:26 2005 +0200
@@ -1,13 +1,14 @@
-(* Title: CCL/terms.thy
+(* Title: CCL/Term.thy
ID: $Id$
Author: Martin Coen
Copyright 1993 University of Cambridge
-
-Definitions of usual program constructs in CCL.
-
*)
-Term = CCL +
+header {* Definitions of usual program constructs in CCL *}
+
+theory Term
+imports CCL
+begin
consts
@@ -15,11 +16,13 @@
if :: "[i,i,i]=>i" ("(3if _/ then _/ else _)" [0,0,60] 60)
- inl,inr :: "i=>i"
- when :: "[i,i=>i,i=>i]=>i"
+ inl :: "i=>i"
+ inr :: "i=>i"
+ when :: "[i,i=>i,i=>i]=>i"
split :: "[i,[i,i]=>i]=>i"
- fst,snd,
+ fst :: "i=>i"
+ snd :: "i=>i"
thd :: "i=>i"
zero :: "i"
@@ -32,10 +35,10 @@
lcase :: "[i,i,[i,i]=>i]=>i"
lrec :: "[i,i,[i,i,i]=>i]=>i"
- let :: "[i,i=>i]=>i"
+ "let" :: "[i,i=>i]=>i"
letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i"
letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
- letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
+ letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
syntax
"@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)"
@@ -50,47 +53,7 @@
"@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
[0,0,0,0,0,60] 60)
-consts
- napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56)
-
-rules
-
- one_def "one == true"
- if_def "if b then t else u == case(b,t,u,% x y. bot,%v. bot)"
- inl_def "inl(a) == <true,a>"
- inr_def "inr(b) == <false,b>"
- when_def "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))"
- split_def "split(t,f) == case(t,bot,bot,f,%u. bot)"
- fst_def "fst(t) == split(t,%x y. x)"
- snd_def "snd(t) == split(t,%x y. y)"
- thd_def "thd(t) == split(t,%x p. split(p,%y z. z))"
- zero_def "zero == inl(one)"
- succ_def "succ(n) == inr(n)"
- ncase_def "ncase(n,b,c) == when(n,%x. b,%y. c(y))"
- nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)"
- nil_def "[] == inl(one)"
- cons_def "h$t == inr(<h,t>)"
- lcase_def "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))"
- lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)"
-
- 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)))"
- letrec_def
- "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)"
-
- letrec2_def "letrec g x y be h(x,y,g) in f(g)==
- letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>)))
- in f(%x y. g'(<x,y>))"
-
- letrec3_def "letrec g x y z be h(x,y,z,g) in f(g) ==
- letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>))))
- in f(%x y z. g'(<x,<y,z>>))"
-
- napply_def "f ^n` a == nrec(n,a,%x g. f(g))"
-
-end
-
-ML
-
+ML {*
(** Quantifier translations: variable binding **)
(* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
@@ -100,11 +63,11 @@
let val (id',b') = variant_abs(id,T,b)
in Const("@let",dummyT) $ Free(id',T) $ a $ b' end;
-fun letrec_tr [Free(f,S),Free(x,T),a,b] =
+fun letrec_tr [Free(f,S),Free(x,T),a,b] =
Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
-fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] =
+fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] =
Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
-fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] =
+fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] =
Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
@@ -128,15 +91,57 @@
in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
end;
-val parse_translation=
- [("@let", let_tr),
- ("@letrec", letrec_tr),
- ("@letrec2", letrec2_tr),
- ("@letrec3", letrec3_tr)
- ];
-val print_translation=
- [("let", let_tr'),
- ("letrec", letrec_tr'),
- ("letrec2", letrec2_tr'),
- ("letrec3", letrec3_tr')
- ];
+*}
+
+parse_translation {*
+ [("@let", let_tr),
+ ("@letrec", letrec_tr),
+ ("@letrec2", letrec2_tr),
+ ("@letrec3", letrec3_tr)] *}
+
+print_translation {*
+ [("let", let_tr'),
+ ("letrec", letrec_tr'),
+ ("letrec2", letrec2_tr'),
+ ("letrec3", letrec3_tr')] *}
+
+consts
+ napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56)
+
+axioms
+
+ one_def: "one == true"
+ if_def: "if b then t else u == case(b,t,u,% x y. bot,%v. bot)"
+ inl_def: "inl(a) == <true,a>"
+ inr_def: "inr(b) == <false,b>"
+ when_def: "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))"
+ split_def: "split(t,f) == case(t,bot,bot,f,%u. bot)"
+ fst_def: "fst(t) == split(t,%x y. x)"
+ snd_def: "snd(t) == split(t,%x y. y)"
+ thd_def: "thd(t) == split(t,%x p. split(p,%y z. z))"
+ zero_def: "zero == inl(one)"
+ succ_def: "succ(n) == inr(n)"
+ ncase_def: "ncase(n,b,c) == when(n,%x. b,%y. c(y))"
+ nrec_def: " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)"
+ nil_def: "[] == inl(one)"
+ cons_def: "h$t == inr(<h,t>)"
+ lcase_def: "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))"
+ lrec_def: "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)"
+
+ 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)))"
+ letrec_def:
+ "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)"
+
+ letrec2_def: "letrec g x y be h(x,y,g) in f(g)==
+ letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>)))
+ in f(%x y. g'(<x,y>))"
+
+ letrec3_def: "letrec g x y z be h(x,y,z,g) in f(g) ==
+ letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>))))
+ in f(%x y z. g'(<x,<y,z>>))"
+
+ napply_def: "f ^n` a == nrec(n,a,%x g. f(g))"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
+end