(* Title: CCL/Type.thy ID: $Id: Type.thy,v 1.7 2005/09/17 15:35:29 wenzelm Exp $ Author: Martin Coen Copyright 1993 University of Cambridge *) header {* Types in CCL are defined as sets of terms *} theory Type imports Term begin consts Subtype :: "['a set, 'a => o] => 'a set" Bool :: "i set" Unit :: "i set" "+" :: "[i set, i set] => i set" (infixr 55) Pi :: "[i set, i => i set] => i set" Sigma :: "[i set, i => i set] => i set" Nat :: "i set" List :: "i set => i set" Lists :: "i set => i set" ILists :: "i set => i set" TAll :: "(i set => i set) => i set" (binder "TALL " 55) TEx :: "(i set => i set) => i set" (binder "TEX " 55) Lift :: "i set => i set" ("(3[_])") SPLIT :: "[i, [i, i] => i set] => i set" syntax "@Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)" [0,0,60] 60) "@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{_: _ ./ _})") translations "PROD x:A. B" => "Pi(A, %x. B)" "A -> B" => "Pi(A, _K(B))" "SUM x:A. B" => "Sigma(A, %x. B)" "A * B" => "Sigma(A, _K(B))" "{x: A. B}" == "Subtype(A, %x. B)" print_translation {* [("Pi", dependent_tr' ("@Pi", "@->")), ("Sigma", dependent_tr' ("@Sigma", "@*"))] *} 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)" 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)})" ML {* use_legacy_bindings (the_context ()) *} end
theorem subsetXH:
A <= B <-> (∀x. x : A --> x : B)
theorem SubtypeI:
[| a : A; P(a) |] ==> a : Subtype(A, P)
theorem SubtypeE:
[| a : Subtype(A, P); [| a : A; P(a) |] ==> Q |] ==> Q
theorem idM:
mono(%X. X)
theorem constM:
mono(%X. A)
theorem LiftM:
mono(A) ==> mono(%X. [A(X)])
theorem SgM:
[| mono(A); !!x X. x : A(X) ==> mono(%X. B(X, x)) |] ==> mono(%X. Sigma(A(X), B(X)))
theorem PiM:
(!!x. x : A ==> mono(%X. B(X, x))) ==> mono(%X. Pi(A, B(X)))
theorem PlusM:
[| mono(A); mono(B) |] ==> mono(%X. A(X) + B(X))
theorem NatM:
mono(op +(Unit))
theorem def_NatB:
Nat = Unit + Nat
theorem ListM:
mono(%X. Unit + A * X)
theorem def_ListB:
List(A) = Unit + A * List(A)
theorem def_ListsB:
Lists(A) = Unit + A * Lists(A)
theorem IListsM:
mono(%X. {} + A * X)
theorem def_IListsB:
ILists(A) = {} + A * ILists(A)
theorem SgE2:
[| <a,b> : Sigma(A, B); [| a : A; b : B(a) |] ==> P |] ==> P
theorem lfp_subset_gfp:
mono(f) ==> lfp(f) <= gfp(f)
theorem gfpI:
[| a : A; !!x X. [| x : A; ALL y:A. t(y) : X |] ==> t(x) : B(X) |] ==> t(a) : gfp(B)
theorem def_gfpI:
[| C == gfp(B); a : A; !!x X. [| x : A; ALL y:A. t(y) : X |] ==> t(x) : B(X) |] ==> t(a) : C