# Theory Type

Up to index of Isabelle/HOL/Lambda

theory Type
imports ListApplication
begin

    (*  Title:      HOL/Lambda/Type.thy
        ID:         $Id: Type.thy,v 1.31 2005/09/22 21:56:35 nipkow Exp $
        Author:     Stefan Berghofer
        Copyright   2000 TU Muenchen
    *)

    header {* Simply-typed lambda terms *}

    theory Type imports ListApplication begin

    subsection {* Environments *}

    constdefs
      shift :: "(nat => 'a) => nat => 'a => nat => 'a"    ("_<_:_>" [90, 0, 0] 91)
      "e<i:a> ≡ λj. if j < i then e j else if j = i then a else e (j - 1)"
    syntax (xsymbols)
      shift :: "(nat => 'a) => nat => 'a => nat => 'a"    ("_⟨_:_⟩" [90, 0, 0] 91)
    syntax (HTML output)
      shift :: "(nat => 'a) => nat => 'a => nat => 'a"    ("_⟨_:_⟩" [90, 0, 0] 91)

    lemma shift_eq [simp]: "i = j ==> (e⟨i:T⟩) j = T"
      by (simp add: shift_def)

    lemma shift_gt [simp]: "j < i ==> (e⟨i:T⟩) j = e j"
      by (simp add: shift_def)

    lemma shift_lt [simp]: "i < j ==> (e⟨i:T⟩) j = e (j - 1)"
      by (simp add: shift_def)

    lemma shift_commute [simp]: "e⟨i:U⟩⟨0:T⟩ = e⟨0:T⟩⟨Suc i:U⟩"
      apply (rule ext)
      apply (case_tac x)
       apply simp
      apply (case_tac nat)
       apply (simp_all add: shift_def)
      done

    subsection {* Types and typing rules *}

    datatype type =
        Atom nat
      | Fun type type    (infixr "=>" 200)

    consts
      typing :: "((nat => type) × dB × type) set"
      typings :: "(nat => type) => dB list => type list => bool"

    syntax
      "_funs" :: "type list => type => type"    (infixr "=>>" 200)
      "_typing" :: "(nat => type) => dB => type => bool"    ("_ |- _ : _" [50, 50, 50] 50)
      "_typings" :: "(nat => type) => dB list => type list => bool"
        ("_ ||- _ : _" [50, 50, 50] 50)
    syntax (xsymbols)
      "_typing" :: "(nat => type) => dB => type => bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    syntax (latex)
      "_funs" :: "type list => type => type"    (infixr "\<Rrightarrow>" 200)
      "_typings" :: "(nat => type) => dB list => type list => bool"
        ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
    translations
      "Ts \<Rrightarrow> T" \<rightleftharpoons> "foldr Fun Ts T"
      "env \<turnstile> t : T" \<rightleftharpoons> "(env, t, T) ∈ typing"
      "env \<tturnstile> ts : Ts" \<rightleftharpoons> "typings env ts Ts"

    inductive typing
      intros
        Var [intro!]: "env x = T ==> env \<turnstile> Var x : T"
        Abs [intro!]: "env⟨0:T⟩ \<turnstile> t : U ==> env \<turnstile> Abs t : (T => U)"
        App [intro!]: "env \<turnstile> s : T => U ==> env \<turnstile> t : T ==> env \<turnstile> (s ° t) : U"

    inductive_cases typing_elims [elim!]:
      "e \<turnstile> Var i : T"
      "e \<turnstile> t ° u : T"
      "e \<turnstile> Abs t : T"

    primrec
      "(e \<tturnstile> [] : Ts) = (Ts = [])"
      "(e \<tturnstile> (t # ts) : Ts) =
        (case Ts of
          [] => False
        | T # Ts => e \<turnstile> t : T ∧ e \<tturnstile> ts : Ts)"

    subsection {* Some examples *}

    lemma "e \<turnstile> Abs (Abs (Abs (Var 1 ° (Var 2 ° Var 1 ° Var 0)))) : ?T"
      by force

    lemma "e \<turnstile> Abs (Abs (Abs (Var 2 ° Var 0 ° (Var 1 ° Var 0)))) : ?T"
      by force

    subsection {* Lists of types *}

    lemma lists_typings:
        "!!Ts. e \<tturnstile> ts : Ts ==> ts ∈ lists {t. ∃T. e \<turnstile> t : T}"
      apply (induct ts)
       apply (case_tac Ts)
         apply simp
         apply (rule lists.Nil)
        apply simp
      apply (case_tac Ts)
       apply simp
      apply simp
      apply (rule lists.Cons)
       apply blast
      apply blast
      done

    lemma types_snoc: "!!Ts. e \<tturnstile> ts : Ts ==> e \<turnstile> t : T ==> e \<tturnstile> ts @ [t] : Ts @ [T]"
      apply (induct ts)
      apply simp
      apply (case_tac Ts)
      apply simp+
      done

    lemma types_snoc_eq: "!!Ts. e \<tturnstile> ts @ [t] : Ts @ [T] =
      (e \<tturnstile> ts : Ts ∧ e \<turnstile> t : T)"
      apply (induct ts)
      apply (case_tac Ts)
      apply simp+
      apply (case_tac Ts)
      apply (case_tac "ts @ [t]")
      apply simp+
      done

    lemma rev_exhaust2 [case_names Nil snoc, extraction_expand]:
      "(xs = [] ==> P) ==> (!!ys y. xs = ys @ [y] ==> P) ==> P"
      -- {* Cannot use @{text rev_exhaust} from the @{text List}
        theory, since it is not constructive *}
      apply (subgoal_tac "∀ys. xs = rev ys --> P")
      apply (erule_tac x="rev xs" in allE)
      apply simp
      apply (rule allI)
      apply (rule impI)
      apply (case_tac ys)
      apply simp
      apply simp
      apply atomize
      apply (erule allE)+
      apply (erule mp, rule conjI)
      apply (rule refl)+
      done

    lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts ==>
      (!!Us U. Ts = Us @ [U] ==> e \<tturnstile> ts : Us ==> e \<turnstile> t : U ==> P) ==> P"
      apply (cases Ts rule: rev_exhaust2)
      apply simp
      apply (case_tac "ts @ [t]")
      apply (simp add: types_snoc_eq)+
      apply iprover
      done

    subsection {* n-ary function types *}

    lemma list_app_typeD:
        "!!t T. e \<turnstile> t °° ts : T ==> ∃Ts. e \<turnstile> t : Ts \<Rrightarrow> T ∧ e \<tturnstile> ts : Ts"
      apply (induct ts)
       apply simp
      apply atomize
      apply simp
      apply (erule_tac x = "t ° a" in allE)
      apply (erule_tac x = T in allE)
      apply (erule impE)
       apply assumption
      apply (elim exE conjE)
      apply (ind_cases "e \<turnstile> t ° u : T")
      apply (rule_tac x = "Ta # Ts" in exI)
      apply simp
      done

    lemma list_app_typeE:
      "e \<turnstile> t °° ts : T ==> (!!Ts. e \<turnstile> t : Ts \<Rrightarrow> T ==> e \<tturnstile> ts : Ts ==> C) ==> C"
      by (insert list_app_typeD) fast

    lemma list_app_typeI:
        "!!t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T ==> e \<tturnstile> ts : Ts ==> e \<turnstile> t °° ts : T"
      apply (induct ts)
       apply simp
      apply atomize
      apply (case_tac Ts)
       apply simp
      apply simp
      apply (erule_tac x = "t ° a" in allE)
      apply (erule_tac x = T in allE)
      apply (erule_tac x = list in allE)
      apply (erule impE)
       apply (erule conjE)
       apply (erule typing.App)
       apply assumption
      apply blast
      done

    text {*
    For the specific case where the head of the term is a variable,
    the following theorems allow to infer the types of the arguments
    without analyzing the typing derivation. This is crucial
    for program extraction.
    *}

    theorem var_app_type_eq:
      "!!T U. e \<turnstile> Var i °° ts : T ==> e \<turnstile> Var i °° ts : U ==> T = U"
      apply (induct ts rule: rev_induct)
      apply simp
      apply (ind_cases "e \<turnstile> Var i : T")
      apply (ind_cases "e \<turnstile> Var i : T")
      apply simp
      apply simp
      apply (ind_cases "e \<turnstile> t ° u : T")
      apply (ind_cases "e \<turnstile> t ° u : T")
      apply atomize
      apply (erule_tac x="Ta => T" in allE)
      apply (erule_tac x="Tb => U" in allE)
      apply (erule impE)
      apply assumption
      apply (erule impE)
      apply assumption
      apply simp
      done

    lemma var_app_types: "!!ts Ts U. e \<turnstile> Var i °° ts °° us : T ==> e \<tturnstile> ts : Ts ==>
      e \<turnstile> Var i °° ts : U ==> ∃Us. U = Us \<Rrightarrow> T ∧ e \<tturnstile> us : Us"
      apply (induct us)
      apply simp
      apply (erule var_app_type_eq)
      apply assumption
      apply simp
      apply atomize
      apply (case_tac U)
      apply (rule FalseE)
      apply simp
      apply (erule list_app_typeE)
      apply (ind_cases "e \<turnstile> t ° u : T")
      apply (drule_tac T="Atom nat" and U="Ta => Tsa \<Rrightarrow> T" in var_app_type_eq)
      apply assumption
      apply simp
      apply (erule_tac x="ts @ [a]" in allE)
      apply (erule_tac x="Ts @ [type1]" in allE)
      apply (erule_tac x="type2" in allE)
      apply simp
      apply (erule impE)
      apply (rule types_snoc)
      apply assumption
      apply (erule list_app_typeE)
      apply (ind_cases "e \<turnstile> t ° u : T")
      apply (drule_tac T="type1 => type2" and U="Ta => Tsa \<Rrightarrow> T" in var_app_type_eq)
      apply assumption
      apply simp
      apply (erule impE)
      apply (rule typing.App)
      apply assumption
      apply (erule list_app_typeE)
      apply (ind_cases "e \<turnstile> t ° u : T")
      apply (frule_tac T="type1 => type2" and U="Ta => Tsa \<Rrightarrow> T" in var_app_type_eq)
      apply assumption
      apply simp
      apply (erule exE)
      apply (rule_tac x="type1 # Us" in exI)
      apply simp
      apply (erule list_app_typeE)
      apply (ind_cases "e \<turnstile> t ° u : T")
      apply (frule_tac T="type1 => Us \<Rrightarrow> T" and U="Ta => Tsa \<Rrightarrow> T" in var_app_type_eq)
      apply assumption
      apply simp
      done

    lemma var_app_typesE: "e \<turnstile> Var i °° ts : T ==>
      (!!Ts. e \<turnstile> Var i : Ts \<Rrightarrow> T ==> e \<tturnstile> ts : Ts ==> P) ==> P"
      apply (drule var_app_types [of _ _ "[]", simplified])
      apply (iprover intro: typing.Var)+
      done

    lemma abs_typeE: "e \<turnstile> Abs t : T ==> (!!U V. e⟨0:U⟩ \<turnstile> t : V ==> P) ==> P"
      apply (cases T)
      apply (rule FalseE)
      apply (erule typing.elims)
      apply simp_all
      apply atomize
      apply (erule_tac x="type1" in allE)
      apply (erule_tac x="type2" in allE)
      apply (erule mp)
      apply (erule typing.elims)
      apply simp_all
      done

    subsection {* Lifting preserves well-typedness *}

    lemma lift_type [intro!]: "e \<turnstile> t : T ==> (!!i U. e⟨i:U⟩ \<turnstile> lift t i : T)"
      by (induct set: typing) auto

    lemma lift_types:
      "!!Ts. e \<tturnstile> ts : Ts ==> e⟨i:U⟩ \<tturnstile> (map (λt. lift t i) ts) : Ts"
      apply (induct ts)
       apply simp
      apply (case_tac Ts)
       apply auto
      done

    subsection {* Substitution lemmas *}

    lemma subst_lemma:
        "e \<turnstile> t : T ==> (!!e' i U u. e' \<turnstile> u : U ==> e = e'⟨i:U⟩ ==> e' \<turnstile> t[u/i] : T)"
      apply (induct set: typing)
        apply (rule_tac x = x and y = i in linorder_cases)
          apply auto
      apply blast
      done

    lemma substs_lemma:
      "!!Ts. e \<turnstile> u : T ==> e⟨i:T⟩ \<tturnstile> ts : Ts ==>
         e \<tturnstile> (map (λt. t[u/i]) ts) : Ts"
      apply (induct ts)
       apply (case_tac Ts)
        apply simp
       apply simp
      apply atomize
      apply (case_tac Ts)
       apply simp
      apply simp
      apply (erule conjE)
      apply (erule (1) subst_lemma)
      apply (rule refl)
      done

    subsection {* Subject reduction *}

    lemma subject_reduction: "e \<turnstile> t : T ==> (!!t'. t -> t' ==> e \<turnstile> t' : T)"
      apply (induct set: typing)
        apply blast
       apply blast
      apply atomize
      apply (ind_cases "s ° t -> t'")
        apply hypsubst
        apply (ind_cases "env \<turnstile> Abs t : T => U")
        apply (rule subst_lemma)
          apply assumption
         apply assumption
        apply (rule ext)
        apply (case_tac x)
         apply auto
      done

    theorem subject_reduction': "t ->β* t' ==> e \<turnstile> t : T ==> e \<turnstile> t' : T"
      by (induct set: rtrancl) (iprover intro: subject_reduction)+

    subsection {* Alternative induction rule for types *}

    lemma type_induct [induct type]:
      "(!!T. (!!T1 T2. T = T1 => T2 ==> P T1) ==>
       (!!T1 T2. T = T1 => T2 ==> P T2) ==> P T) ==> P T"
    proof -
      case rule_context
      show ?thesis
      proof (induct T)
        case Atom
        show ?case by (rule rule_context) simp_all
      next
        case Fun
        show ?case  by (rule rule_context) (insert Fun, simp_all)
      qed
    qed

    end

### Environments

lemma shift_eq:

      i = j ==> (e⟨i:T⟩) j = T

lemma shift_gt:

      j < i ==> (e⟨i:T⟩) j = e j

lemma shift_lt:

      i < j ==> (e⟨i:T⟩) j = e (j - 1)

lemma shift_commute:

      e⟨i:U⟩⟨0:T⟩ = e⟨0:T⟩⟨Suc i:U⟩

### Types and typing rules

lemmas typing_elims:

      [| e |- Var i : T; T = e i ==> P |] ==> P

      [| e |- t ° u : T; !!T. [| e |- t : T => T; e |- u : T |] ==> P |] ==> P

      [| e |- Abs t : T; !!T U. [| e⟨0:T⟩ |- t : U; T = T => U |] ==> P |] ==> P

### Some examples

lemma

      e |- Abs (Abs (Abs (Var 1 °
                          (Var 2 ° Var 1 °
                           Var 0)))) : ((Ta => U) => T => Ta) => (Ta => U) => T => U

lemma

      e |- Abs (Abs (Abs (Var 2 ° Var 0 °
                          (Var 1 ° Var 0)))) : (T => Ta => U) => (T => Ta) => T => U

### Lists of types

lemma lists_typings:

      e ||- ts : Ts ==> ts ∈ lists {t. ∃T. e |- t : T}

lemma types_snoc:

      [| e ||- ts : Ts; e |- t : T |] ==> e ||- ts @ [t] : Ts @ [T]

lemma types_snoc_eq:

      (e ||- ts @ [t] : Ts @ [T]) = (e ||- ts : Ts ∧ e |- t : T)

lemma rev_exhaust2:

      [| xs = [] ==> P; !!ys y. xs = ys @ [y] ==> P |] ==> P

lemma types_snocE:

      [| e ||- ts @ [t] : Ts;
         !!Us U. [| Ts = Us @ [U]; e ||- ts : Us; e |- t : U |] ==> P |]
      ==> P

### n-ary function types

lemma list_app_typeD:

      e |- t °° ts : T ==> ∃Ts. e |- t : Ts =>> T ∧ e ||- ts : Ts

lemma list_app_typeE:

      [| e |- t °° ts : T; !!Ts. [| e |- t : Ts =>> T; e ||- ts : Ts |] ==> C |] ==> C

lemma list_app_typeI:

      [| e |- t : Ts =>> T; e ||- ts : Ts |] ==> e |- t °° ts : T

theorem var_app_type_eq:

      [| e |- Var i °° ts : T; e |- Var i °° ts : U |] ==> T = U

lemma var_app_types:

      [| e |- Var i °° ts °° us : T; e ||- ts : Ts; e |- Var i °° ts : U |]
      ==> ∃Us. U = Us =>> T ∧ e ||- us : Us

lemma var_app_typesE:

      [| e |- Var i °° ts : T;
         !!Ts. [| e |- Var i : Ts =>> T; e ||- ts : Ts |] ==> P |]
      ==> P

lemma abs_typeE:

      [| e |- Abs t : T; !!U V. e⟨0:U⟩ |- t : V ==> P |] ==> P

### Lifting preserves well-typedness

lemma lift_type:

      e |- t : T ==> e⟨i:U⟩ |- lift t i : T

lemma lift_types:

      e ||- ts : Ts ==> e⟨i:U⟩ ||- map (%t. lift t i) ts : Ts

### Substitution lemmas

lemma subst_lemma:

      [| e |- t : T; e' |- u : U; e = e'⟨i:U⟩ |] ==> e' |- t[u/i] : T

lemma substs_lemma:

      [| e |- u : T; e⟨i:T⟩ ||- ts : Ts |] ==> e ||- map (%t. t[u/i]) ts : Ts

### Subject reduction

lemma subject_reduction:

      [| e |- t : T; t -> t' |] ==> e |- t' : T

theorem subject_reduction':

      [| t ->> t'; e |- t : T |] ==> e |- t' : T

### Alternative induction rule for types

lemma type_induct:

      (!!T. [| !!T1 T2. T = T1 => T2 ==> P T1; !!T1 T2. T = T1 => T2 ==> P T2 |]
            ==> P T)
      ==> P T