src/HOL/Lambda/Type.thy

new 'THEN' syntax;

(*  Title:      HOL/Lambda/Type.thy
    ID:         $Id$
    Author:     Stefan Berghofer
    Copyright   2000 TU Muenchen
*)

header {* Simply-typed lambda terms: subject reduction and strong
  normalization *}

theory Type = InductTermi:

text_raw {*
  \footnote{Formalization by Stefan Berghofer.  Partly based on a
  paper proof by Ralph Matthes.}
*}


subsection {* Types and typing rules *}

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

consts
  typing :: "((nat => type) \<times> dB \<times> type) set"

syntax
  "_typing" :: "[nat => type, dB, type] => bool"  ("_ |- _ : _" [50,50,50] 50)
  "_funs" :: "[type list, type] => type"  (infixl "=>>" 150)
translations
  "env |- t : T" == "(env, t, T) \<in> typing"
  "Ts =>> T" == "foldr Fun Ts T"

inductive typing
  intros [intro!]
    Var: "env x = T ==> env |- Var x : T"
    Abs: "(nat_case T env) |- t : U ==> env |- Abs t : (T => U)"
    App: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"

inductive_cases [elim!]:
  "e |- Var i : T"
  "e |- t $ u : T"
  "e |- Abs t : T"

consts
  "types" :: "[nat => type, dB list, type list] => bool"
primrec
  "types e [] Ts = (Ts = [])"
  "types e (t # ts) Ts =
    (case Ts of
      [] => False
    | T # Ts => e |- t : T \<and> types e ts Ts)"

inductive_cases [elim!]:
  "x # xs \<in> lists S"

declare IT.intros [intro!]


subsection {* Some examples *}

lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : T \<and> U = T"
  apply (intro exI conjI)
   apply force
  apply (rule refl)
  done

lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : T \<and> U = T";
  apply (intro exI conjI)
   apply force
  apply (rule refl)
  done


text {* Iterated function types *}

lemma list_app_typeD [rule_format]:
    "\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)"
  apply (induct_tac ts)
   apply simp
  apply (intro strip)
  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 |- t $ u : T")
  apply (rule_tac x = "Ta # Ts" in exI)
  apply simp
  done

lemma list_app_typeI [rule_format]:
    "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
  apply (induct_tac ts)
   apply (intro strip)
   apply simp
  apply (intro strip)
  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 = lista in allE)
  apply (erule impE)
   apply (erule conjE)
   apply (erule typing.App)
   apply assumption
  apply blast
  done

lemma lists_types [rule_format]:
    "\<forall>Ts. types e ts Ts --> ts \<in> lists {t. \<exists>T. e |- t : T}"
  apply (induct_tac ts)
   apply (intro strip)
   apply (case_tac Ts)
     apply simp
     apply (rule lists.Nil)
    apply simp
  apply (intro strip)
  apply (case_tac Ts)
   apply simp
  apply simp
  apply (rule lists.Cons)
   apply blast
  apply blast
  done


subsection {* Lifting preserves termination and well-typedness *}

lemma lift_map [rule_format, simp]:
    "\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
  apply (induct_tac ts)
   apply simp_all
  done

lemma subst_map [rule_format, simp]:
  "\<forall>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts"
  apply (induct_tac ts)
   apply simp_all
  done

lemma lift_IT [rule_format, intro!]:
    "t \<in> IT ==> \<forall>i. lift t i \<in> IT"
  apply (erule IT.induct)
    apply (rule allI)
    apply (simp (no_asm))
    apply (rule conjI)
     apply
      (rule impI,
       rule IT.Var,
       erule lists.induct,
       simp (no_asm),
       rule lists.Nil,
       simp (no_asm),
       erule IntE,
       rule lists.Cons,
       blast,
       assumption)+
     apply auto
   done

lemma lifts_IT [rule_format]:
    "ts \<in> lists IT --> map (\<lambda>t. lift t 0) ts \<in> lists IT"
  apply (induct_tac ts)
   apply auto
  done


lemma shift_env [simp]:
  "nat_case T
    (\<lambda>j. if j < i then e j else if j = i then Ua else e (j - 1)) =
    (\<lambda>j. if j < Suc i then nat_case T e j else if j = Suc i then Ua
          else nat_case T e (j - 1))"
  apply (rule ext)
  apply (case_tac j)
   apply simp
  apply (case_tac nat)
   apply simp_all
  done

lemma lift_type' [rule_format]:
  "e |- t : T ==> \<forall>i U.
    (\<lambda>j. if j < i then e j
          else if j = i then U
          else e (j - 1)) |- lift t i : T"
  apply (erule typing.induct)
    apply auto
  done

lemma lift_type [intro!]:
    "e |- t : T ==> nat_case U e |- lift t 0 : T"
  apply (subgoal_tac
    "nat_case U e =
      (\<lambda>j. if j < 0 then e j
            else if j = 0 then U else e (j - 1))")
   apply (erule ssubst)
   apply (erule lift_type')
  apply (rule ext)
  apply (case_tac j)
   apply simp_all
  done

lemma lift_types [rule_format]:
  "\<forall>Ts. types e ts Ts -->
    types (\<lambda>j. if j < i then e j
                else if j = i then U
                else e (j - 1)) (map (\<lambda>t. lift t i) ts) Ts"
  apply (induct_tac ts)
   apply simp
  apply (intro strip)
  apply (case_tac Ts)
   apply simp_all
  apply (rule lift_type')
  apply (erule conjunct1)
  done


subsection {* Substitution lemmas *}

lemma subst_lemma [rule_format]:
  "e |- t : T ==> \<forall>e' i U u.
    e = (\<lambda>j. if j < i then e' j
              else if j = i then U
              else e' (j-1)) -->
    e' |- u : U --> e' |- t[u/i] : T"
  apply (erule typing.induct)
    apply (intro strip)
    apply (case_tac "x = i")
     apply simp
    apply (frule linorder_neq_iff [THEN iffD1])
    apply (erule disjE)
     apply simp
     apply (rule typing.Var)
     apply assumption
    apply (frule order_less_not_sym)
    apply (simp only: subst_gt split: split_if add: if_False)
    apply (rule typing.Var)
    apply assumption
   apply fastsimp
  apply fastsimp
  done

lemma substs_lemma [rule_format]:
  "e |- u : T ==>
    \<forall>Ts. types (\<lambda>j. if j < i then e j
                     else if j = i then T else e (j - 1)) ts Ts -->
      types e (map (\<lambda>t. t[u/i]) ts) Ts"
  apply (induct_tac ts)
   apply (intro strip)
   apply (case_tac Ts)
    apply simp
   apply simp
  apply (intro strip)
  apply (case_tac Ts)
   apply simp
  apply simp
  apply (erule conjE)
  apply (erule subst_lemma)
   apply (rule refl)
  apply assumption
  done


subsection {* Subject reduction *}

lemma subject_reduction [rule_format]:
    "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T"
  apply (erule typing.induct)
    apply blast
   apply blast
  apply (intro strip)
  apply (ind_cases "s $ t -> t'")
    apply hypsubst
    apply (ind_cases "env |- Abs t : T => U")
    apply (rule subst_lemma)
      apply assumption
     prefer 2
     apply assumption
    apply (rule ext)
    apply (case_tac j)
     apply auto
  done


subsection {* Additional lemmas *}

lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])"
  apply simp
  done

lemma subst_Var_IT [rule_format]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
  apply (erule IT.induct)
    txt {* Case @{term Var}: *}
    apply (intro strip)
    apply (simp (no_asm) add: subst_Var)
    apply
    ((rule conjI impI)+,
      rule IT.Var,
      erule lists.induct,
      simp (no_asm),
      rule lists.Nil,
      simp (no_asm),
      erule IntE,
      erule CollectE,
      rule lists.Cons,
      fast,
      assumption)+
   txt {* Case @{term Lambda}: *}
   apply (intro strip)
   apply simp
   apply (rule IT.Lambda)
   apply fast
  txt {* Case @{term Beta}: *}
  apply (intro strip)
  apply (simp (no_asm_use) add: subst_subst [symmetric])
  apply (rule IT.Beta)
   apply auto
  done

lemma Var_IT: "Var n \<in> IT"
  apply (subgoal_tac "Var n $$ [] \<in> IT")
   apply simp
  apply (rule IT.Var)
  apply (rule lists.Nil)
  done

lemma app_Var_IT: "t \<in> IT ==> t $ Var i \<in> IT"
  apply (erule IT.induct)
    apply (subst app_last)
    apply (rule IT.Var)
    apply simp
    apply (rule lists.Cons)
     apply (rule Var_IT)
    apply (rule lists.Nil)
   apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]])
    apply (erule subst_Var_IT)
   apply (rule Var_IT)
  apply (subst app_last)
  apply (rule IT.Beta)
   apply (subst app_last [symmetric])
   apply assumption
  apply assumption
  done


subsection {* Well-typed substitution preserves termination *}

lemma subst_type_IT [rule_format]:
  "\<forall>t. t \<in> IT --> (\<forall>e T u i.
    (\<lambda>j. if j < i then e j
          else if j = i then U
          else e (j - 1)) |- t : T -->
    u \<in> IT --> e |- u : U --> t[u/i] \<in> IT)"
  apply (rule_tac f = size and a = U in measure_induct)
  apply (rule allI)
  apply (rule impI)
  apply (erule IT.induct)
    txt {* Case @{term Var}: *}
    apply (intro strip)
    apply (case_tac "n = i")
     txt {* Case @{term "n = i"}: *}
     apply (case_tac rs)
      apply simp
     apply simp
     apply (drule list_app_typeD)
     apply (elim exE conjE)
     apply (ind_cases "e |- t $ u : T")
     apply (ind_cases "e |- Var i : T")
     apply (drule_tac s = "(?T::type) => ?U" in sym)
     apply simp
     apply (subgoal_tac "lift u 0 $ Var 0 \<in> IT")
      prefer 2
      apply (rule app_Var_IT)
      apply (erule lift_IT)
     apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] \<in> IT")
      apply (simp (no_asm_use))
      apply (subgoal_tac "(Var 0 $$ map (\<lambda>t. lift t 0)
        (map (\<lambda>t. t[u/i]) list))[(u $ a[u/i])/0] \<in> IT")
       apply (simp (no_asm_use) del: map_compose
	 add: map_compose [symmetric] o_def)
      apply (erule_tac x = "Ts =>> T" in allE)
      apply (erule impE)
       apply simp
      apply (erule_tac x = "Var 0 $$
        map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) list)" in allE)
      apply (erule impE)
       apply (rule IT.Var)
       apply (rule lifts_IT)
       apply (drule lists_types)
       apply
        (ind_cases "x # xs \<in> lists (Collect P)",
         erule lists_IntI [THEN lists.induct],
         assumption)
        apply fastsimp
       apply fastsimp
      apply (erule_tac x = e in allE)
      apply (erule_tac x = T in allE)
      apply (erule_tac x = "u $ a[u/i]" in allE)
      apply (erule_tac x = 0 in allE)
      apply (fastsimp intro!: list_app_typeI lift_types subst_lemma substs_lemma)
     apply (erule_tac x = Ta in allE)
     apply (erule impE)
      apply simp
     apply (erule_tac x = "lift u 0 $ Var 0" in allE)
     apply (erule impE)
      apply assumption
     apply (erule_tac x = e in allE)
     apply (erule_tac x = "Ts =>> T" in allE)
     apply (erule_tac x = "a[u/i]" in allE)
     apply (erule_tac x = 0 in allE)
     apply (erule impE)
      apply (rule typing.App)
       apply (erule lift_type')
      apply (rule typing.Var)
      apply simp
     apply (fast intro!: subst_lemma)
    txt {* Case @{term "n ~= i"}: *}
    apply (drule list_app_typeD)
    apply (erule exE)
    apply (erule conjE)
    apply (drule lists_types)
    apply (subgoal_tac "map (\<lambda>x. x[u/i]) rs \<in> lists IT")
     apply (simp add: subst_Var)
     apply fast
    apply (erule lists_IntI [THEN lists.induct])
      apply assumption
     apply fastsimp
    apply fastsimp
   txt {* Case @{term Lambda}: *}
   apply fastsimp
  txt {* Case @{term Beta}: *}
  apply (intro strip)
  apply (simp (no_asm))
  apply (rule IT.Beta)
   apply (simp (no_asm) del: subst_map add: subst_subst subst_map [symmetric])
   apply (drule subject_reduction)
    apply (rule apps_preserves_beta)
    apply (rule beta.beta)
   apply fast
  apply (drule list_app_typeD)
  apply fast
  done


subsection {* Main theorem: well-typed terms are strongly normalizing *}

lemma type_implies_IT: "e |- t : T ==> t \<in> IT"
  apply (erule typing.induct)
    apply (rule Var_IT)
   apply (erule IT.Lambda)
  apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] \<in> IT")
   apply simp
  apply (rule subst_type_IT)
  apply (rule lists.Nil
    [THEN [2] lists.Cons [THEN IT.Var], unfolded foldl_Nil [THEN eq_reflection]
      foldl_Cons [THEN eq_reflection]])
      apply (erule lift_IT)
     apply (rule typing.App)
     apply (rule typing.Var)
     apply simp
    apply (erule lift_type')
   apply assumption
  apply assumption
  done

theorem type_implies_termi: "e |- t : T ==> t \<in> termi beta"
  apply (rule IT_implies_termi)
  apply (erule type_implies_IT)
  done

end