# Theory Types

Up to index of Isabelle/ZF/Coind

theory Types
imports Language
begin

    (*  Title:      ZF/Coind/Types.thy
        ID:         $Id: Types.thy,v 1.13 2005/06/17 14:15:10 haftmann Exp $
        Author:     Jacob Frost, Cambridge University Computer Laboratory
        Copyright   1995  University of Cambridge
    *)

    theory Types imports Language begin

    consts
      Ty :: i               (* Datatype of types *)
      TyConst :: i          (* Abstract type of type constants *)

    datatype
      "Ty" = t_const ("tc ∈ TyConst")
           | t_fun ("t1 ∈ Ty","t2 ∈ Ty")

    (* Definition of type environments and associated operators *)

    consts
      TyEnv :: i

    datatype
      "TyEnv" = te_emp
              | te_owr ("te ∈ TyEnv","x ∈ ExVar","t ∈ Ty")

    consts
      te_dom :: "i => i"
      te_app :: "[i,i] => i"

    primrec (*domain of the type environment*)
      "te_dom (te_emp) = 0"
      "te_dom (te_owr(te,x,v)) = te_dom(te) Un {x}"

    primrec (*lookup up identifiers in the type environment*)
      "te_app (te_emp,x) = 0"
      "te_app (te_owr(te,y,t),x) = (if x=y then t else te_app(te,x))"

    inductive_cases te_owrE [elim!]: "te_owr(te,f,t) ∈ TyEnv"

    (*redundant??*)
    lemma te_app_owr1: "te_app(te_owr(te,x,t),x) = t"
    by simp

    (*redundant??*)
    lemma te_app_owr2: "x ≠ y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)"
    by auto

    lemma te_app_owr [simp]:
         "te_app(te_owr(te,x,t),y) = (if x=y then t else te_app(te,y))"
    by auto

    lemma te_appI:
         "[| te ∈ TyEnv; x ∈ ExVar; x ∈ te_dom(te) |] ==> te_app(te,x) ∈ Ty"
    apply (erule_tac P = "x ∈ te_dom (te) " in rev_mp)
    apply (erule TyEnv.induct, auto)
    done

    end

lemmas te_owrE:

      [| te_owr(te, f, t) ∈ TyEnv; [| te ∈ TyEnv; f ∈ ExVar; t ∈ Ty |] ==> Q |] ==> Q

lemma te_app_owr1:

      te_app(te_owr(te, x, t), x) = t

lemma te_app_owr2:

      x ≠ y ==> te_app(te_owr(te, x, t), y) = te_app(te, y)

lemma te_app_owr:

      te_app(te_owr(te, x, t), y) = (if x = y then t else te_app(te, y))

lemma te_appI:

      [| te ∈ TyEnv; x ∈ ExVar; x ∈ te_dom(te) |] ==> te_app(te, x) ∈ Ty