--- a/src/CCL/Type.thy Sat Sep 17 14:02:31 2005 +0200
+++ b/src/CCL/Type.thy Sat Sep 17 17:35:26 2005 +0200
@@ -1,13 +1,14 @@
-(* Title: CCL/types.thy
+(* Title: CCL/Type.thy
ID: $Id$
Author: Martin Coen
Copyright 1993 University of Cambridge
-
-Types in CCL are defined as sets of terms.
-
*)
-Type = Term +
+header {* Types in CCL are defined as sets of terms *}
+
+theory Type
+imports Term
+begin
consts
@@ -33,7 +34,7 @@
"@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)"
[0,0,60] 60)
-
+
"@->" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53)
"@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55)
"@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})")
@@ -45,32 +46,29 @@
"A * B" => "Sigma(A, _K(B))"
"{x: A. B}" == "Subtype(A, %x. B)"
-rules
+print_translation {*
+ [("Pi", dependent_tr' ("@Pi", "@->")),
+ ("Sigma", dependent_tr' ("@Sigma", "@*"))] *}
- Subtype_def "{x:A. P(x)} == {x. x:A & P(x)}"
- Unit_def "Unit == {x. x=one}"
- Bool_def "Bool == {x. x=true | x=false}"
- Plus_def "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
- Pi_def "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}"
- Sigma_def "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
- Nat_def "Nat == lfp(% X. Unit + X)"
- List_def "List(A) == lfp(% X. Unit + A*X)"
+axioms
+ Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"
+ Unit_def: "Unit == {x. x=one}"
+ Bool_def: "Bool == {x. x=true | x=false}"
+ Plus_def: "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
+ Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}"
+ Sigma_def: "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
+ Nat_def: "Nat == lfp(% X. Unit + X)"
+ List_def: "List(A) == lfp(% X. Unit + A*X)"
- Lists_def "Lists(A) == gfp(% X. Unit + A*X)"
- ILists_def "ILists(A) == gfp(% X.{} + A*X)"
+ Lists_def: "Lists(A) == gfp(% X. Unit + A*X)"
+ ILists_def: "ILists(A) == gfp(% X.{} + A*X)"
- Tall_def "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
- Tex_def "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
- Lift_def "[A] == A Un {bot}"
+ Tall_def: "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
+ Tex_def: "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
+ Lift_def: "[A] == A Un {bot}"
- SPLIT_def "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})"
+ SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
-
-
-ML
-
-val print_translation =
- [("Pi", dependent_tr' ("@Pi", "@->")),
- ("Sigma", dependent_tr' ("@Sigma", "@*"))];
-