# Theory Type

Up to index of Isabelle/CCL

theory Type
imports Term
uses [Type.ML]
begin

    (*  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