src/CCL/Type.thy
changeset 17456 bcf7544875b2
parent 14765 bafb24c150c1
child 17782 b3846df9d643
--- 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", "@*"))];
-