# HG changeset patch
# User berghofe
# Date 961755877 -7200
# Node ID de99e37effda242396dfd50402be6e7927193141
# Parent  e221d4f81d52e4c8d0dc93e8b03af9c352e2930e
Subject reduction and strong normalization of simply-typed lambda terms.

diff -r e221d4f81d52 -r de99e37effda src/HOL/Lambda/Type.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/Type.ML	Fri Jun 23 12:24:37 2000 +0200
@@ -0,0 +1,418 @@
+(*  Title:      HOL/Lambda/Type.ML
+    ID:         $Id$
+    Author:     Stefan Berghofer
+    Copyright   2000 TU Muenchen
+
+Subject reduction and strong normalization of simply-typed lambda terms.
+
+Partly based on a paper proof by Ralph Matthes.
+*)
+
+AddSIs IT.intrs;
+AddSIs typing.intrs;
+AddSEs (map typing.mk_cases
+  ["e |- Var i : T", "e |- t $ u : T", "e |- Abs t : T"]);
+AddSEs [lists.mk_cases "x # xs : lists S"];
+
+(*** test ***)
+
+Goal "e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : ?T";
+by (fast_tac (claset() addss simpset()) 1);
+result();
+
+Goal "e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T";
+by (fast_tac (claset() addss simpset()) 1);
+result();
+
+(**** n-ary function types ****)
+
+Goal "ALL t T. \
+  \ e |- t $$ ts : T --> (EX Ts. e |- t : Ts =>> T & types e ts Ts)";
+by (induct_tac "ts" 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (Full_simp_tac 1);
+by (eres_inst_tac [("x","t $ a")] allE 1);
+by (eres_inst_tac [("x","T")] allE 1);
+by (etac impE 1);
+by (assume_tac 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (etac (typing.mk_cases "e |- t $ u : T") 1);
+by (res_inst_tac [("x","Ta # Ts")] exI 1);
+by (Asm_simp_tac 1);
+qed_spec_mp "list_app_typeD";
+
+Goal "ALL t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T";
+by (induct_tac "ts" 1);
+by (strip_tac 1);
+by (Asm_full_simp_tac 1);
+by (strip_tac 1);
+by (case_tac "Ts" 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","t $ a")] allE 1);
+by (eres_inst_tac [("x","T")] allE 1);
+by (eres_inst_tac [("x","lista")] allE 1);
+by (etac impE 1);
+by (etac conjE 1);
+by (etac typing.APP 1);
+by (assume_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "list_app_typeI";
+
+Goal "ALL Ts. types e ts Ts --> ts : lists {t. EX T. e |- t : T}";
+by (induct_tac "ts" 1);
+by (strip_tac 1);
+by (case_tac "Ts" 1);
+by (Asm_full_simp_tac 1);
+by (rtac lists.Nil 1);
+by (Asm_full_simp_tac 1);
+by (strip_tac 1);
+by (case_tac "Ts" 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac lists.Cons 1);
+by (Fast_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "lists_types";
+
+(**** lifting preserves termination and well-typedness ****)
+
+Goal "ALL t. lift (t $$ ts) i = lift t i $$ map (%t. lift t i) ts";
+by (induct_tac "ts" 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed_spec_mp "lift_map";
+
+Goal "ALL t. subst (t $$ ts) u i = subst t u i $$ map (%t. subst t u i) ts";
+by (induct_tac "ts" 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed_spec_mp "subst_map";
+
+Addsimps [lift_map, subst_map];
+
+Goal "t : IT ==> ALL i. lift t i : IT";
+by (etac IT.induct 1);
+by (rtac allI 1);
+by (Simp_tac 1);
+by (rtac conjI 1);
+by (REPEAT (EVERY
+  [rtac impI 1,
+   rtac IT.VarI 1,
+   etac lists.induct 1,
+   Simp_tac 1,
+   rtac lists.Nil 1,
+   Simp_tac 1,
+   etac IntE 1,
+   rtac lists.Cons 1,
+   Fast_tac 1,
+   atac 1]));
+by (ALLGOALS (fast_tac (claset() addss simpset())));
+qed_spec_mp "lift_IT";
+AddSIs [lift_IT];
+
+Goal "ts : lists IT --> map (%t. lift t 0) ts : lists IT";
+by (induct_tac "ts" 1);
+by (ALLGOALS (fast_tac (claset() addss simpset())));
+qed_spec_mp "lifts_IT";
+
+Goal "nat_case T  \
+ \   (%j. if j < i then e j else if j = i then Ua else e (j - 1)) =  \
+ \ (%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))";
+by (rtac ext 1);
+by (case_tac "j" 1);
+by (Asm_simp_tac 1);
+by (case_tac "nat" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "shift_env";
+Addsimps [shift_env];
+
+Goal "e |- t : T ==> ALL i U. \
+  \ (%j. if j < i then e j  \
+  \     else if j = i then U \
+  \     else e (j-1)) |- lift t i : T";
+by (etac typing.induct 1);
+by (ALLGOALS (fast_tac (claset() addss simpset())));
+qed_spec_mp "lift_type'";
+
+Goal "e |- t : T ==> nat_case U e |- lift t 0 : T";
+by (subgoal_tac
+  "nat_case U e = (%j. if j < 0 then e j  \
+ \  else if j = 0 then U else e (j-1))" 1);
+by (etac ssubst 1);
+by (etac lift_type' 1);
+by (rtac ext 1);
+by (case_tac "j" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+qed "lift_type";
+AddSIs [lift_type];
+
+Goal "ALL Ts. types e ts Ts -->  \
+  \ types (%j. if j < i then e j  \
+  \     else if j = i then U \
+  \     else e (j-1)) (map (%t. lift t i) ts) Ts";
+by (induct_tac "ts" 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (case_tac "Ts" 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac lift_type' 1);
+by (etac conjunct1 1);
+qed_spec_mp "lift_types";
+
+(**** substitution lemma ****)
+
+Goal "e |- t : T ==> ALL e' i U u. \
+  \ e = (%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";
+by (etac typing.induct 1);
+by (strip_tac 1);
+by (case_tac "x=i" 1);
+by (Asm_full_simp_tac 1);
+by (ftac (linorder_neq_iff RS iffD1) 1);
+by (etac disjE 1);
+by (Asm_full_simp_tac 1);
+by (rtac typing.VAR 1);
+by (assume_tac 1);
+by (ftac order_less_not_sym 1);
+by (asm_full_simp_tac (HOL_ss addsimps [subst_gt]) 1);
+by (rtac typing.VAR 1);
+by (assume_tac 1);
+by (ALLGOALS (fast_tac (claset() addss simpset())));
+qed_spec_mp "subst_lemma";
+
+Goal "e |- u : T ==> ALL Ts. types (%j. if j < i then e j  \
+  \  else if j = i then T else e (j - 1))  \
+  \ ts Ts --> types e (map (%t. t[u/i]) ts) Ts";
+by (induct_tac "ts" 1);
+by (strip_tac 1);
+by (case_tac "Ts" 1);
+by (Asm_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (strip_tac 1);
+by (case_tac "Ts" 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (etac conjE 1);
+by (etac subst_lemma 1);
+by (rtac refl 1);
+by (assume_tac 1);
+qed_spec_mp "substs_lemma";
+
+(**** subject reduction ****)
+
+Goal "e |- t : T ==> ALL t'. t -> t' --> e |- t' : T";
+by (etac typing.induct 1);
+by (Fast_tac 1);
+by (Fast_tac 1);
+by (strip_tac 1);
+by (etac (beta.mk_cases "s $ t -> t'") 1);
+by (hyp_subst_tac 1);
+by (etac (typing.mk_cases "env |- Abs t : T => U") 1);
+by (rtac subst_lemma 1);
+by (assume_tac 1);
+by (assume_tac 2);
+by (rtac ext 1);
+by (case_tac "j" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Fast_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "subject_reduction";
+
+(**** additional lemmas ****)
+
+Goal "ALL t. (t $$ ts) $ u = t $$ (ts @ [u])";
+by (induct_tac "ts" 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed_spec_mp "app_last";
+
+Goal "ALL ys. xs : lists S --> ys : lists S --> xs @ ys : lists S";
+by (induct_tac "xs" 1);
+by (ALLGOALS (fast_tac (claset() addss simpset())));
+qed_spec_mp "append_lists";
+
+Goal "r : IT ==> ALL i j. r[Var i/j] : IT";
+by (etac IT.induct 1);
+(** Var **)
+by (strip_tac 1);
+by (simp_tac (simpset() addsimps [subst_Var]) 1);
+by (REPEAT (EVERY
+  [REPEAT (resolve_tac [conjI, impI] 1),
+   rtac IT.VarI 1,
+   etac lists.induct 1,
+   Simp_tac 1,
+   rtac lists.Nil 1,
+   Simp_tac 1,
+   etac IntE 1,
+   etac CollectE 1,
+   rtac lists.Cons 1,
+   Fast_tac 1,
+   atac 1]));
+(** Lambda **)
+by (strip_tac 1);
+by (Simp_tac 1);
+by (rtac IT.LambdaI 1);
+by (Fast_tac 1);
+(** Beta **)
+by (strip_tac 1);
+by (full_simp_tac (simpset() addsimps [subst_subst RS sym]) 1);
+by (rtac IT.BetaI 1);
+by (Fast_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "subst_Var_IT";
+
+val Var_IT = rewrite_rule [mk_meta_eq foldl_Nil] (lists.Nil RS IT.VarI);
+
+Goal "t : IT ==> t $ Var i : IT";
+by (etac IT.induct 1);
+by (stac app_last 1);
+by (rtac IT.VarI 1);
+by (rtac append_lists 1);
+by (Asm_full_simp_tac 1);
+by (rtac lists.Cons 1);
+by (rtac Var_IT 1);
+by (rtac lists.Nil 1);
+by (rtac (rewrite_rule [mk_meta_eq foldl_Nil]
+  (read_instantiate [("ss","[]")] IT.BetaI)) 1);
+by (etac subst_Var_IT 1);
+by (rtac Var_IT 1);
+by (stac app_last 1);
+by (rtac IT.BetaI 1);
+by (stac (app_last RS sym) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "app_Var_IT";
+
+(**** well-typed substitution preserves termination ****)
+
+Goal "ALL t. t : IT --> (ALL e T u i. \
+  \  (%j. if j < i then e j  \
+  \       else if j = i then U  \
+  \       else e (j - 1)) |- t : T -->  \
+  \  u : IT --> e |- u : U --> t[u/i] : IT)";
+by (res_inst_tac [("f","size"),("a","U")] measure_induct 1);
+by (rtac allI 1);
+by (rtac impI 1);
+by (etac IT.induct 1);
+(** Var **)
+by (strip_tac 1);
+by (case_tac "n=i" 1);
+(** n=i **)
+by (case_tac "rs" 1);
+by (Asm_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (dtac list_app_typeD 1);
+by (REPEAT (eresolve_tac [exE, conjE] 1));
+by (etac (typing.mk_cases "e |- t $ u : T") 1);
+by (etac (typing.mk_cases "e |- Var i : T") 1);
+by (dres_inst_tac [("s","(?T::typ) => ?U")] sym 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "lift u 0 $ Var 0 : IT" 1);
+by (rtac app_Var_IT 2);
+by (etac lift_IT 2);
+by (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] : IT" 1);
+by (Full_simp_tac 1);
+by (subgoal_tac "(Var 0 $$ map (%t. lift t 0)  \
+  \  (map (%t. t[u/i]) list))[(u $ a[u/i])/0] : IT" 1);
+by (full_simp_tac (simpset() delsimps [map_compose] addsimps
+  [map_compose RS sym, o_def]) 1);
+by (eres_inst_tac [("x", "Ts =>> T")] allE 1);
+by (etac impE 1);
+by (Simp_tac 1);
+by (eres_inst_tac [("x", "Var 0 $$ \
+ \  map (%t. lift t 0) (map (%t. t[u/i]) list)")] allE 1);
+by (etac impE 1);
+by (rtac IT.VarI 1);
+by (rtac lifts_IT 1);
+by (dtac lists_types 1);
+byev [etac (lists.mk_cases "x # xs : lists (Collect P)") 1,
+  etac (lists_IntI RS lists.induct) 1,
+  atac 1];
+by (fast_tac (claset() addss simpset()) 1);
+by (fast_tac (claset() addss simpset()) 1);
+by (eres_inst_tac [("x","e")] allE 1);
+by (eres_inst_tac [("x","T")] allE 1);
+by (eres_inst_tac [("x","u $ a[u/i]")] allE 1);
+by (eres_inst_tac [("x","0")] allE 1);
+by (fast_tac (claset()
+  addSIs [list_app_typeI, lift_types, subst_lemma, substs_lemma]
+  addss simpset()) 1);
+by (eres_inst_tac [("x", "Ta")] allE 1);
+by (etac impE 1);
+by (Simp_tac 1);
+by (eres_inst_tac [("x", "lift u 0 $ Var 0")] allE 1);
+by (etac impE 1);
+by (assume_tac 1);
+by (eres_inst_tac [("x", "e")] allE 1);
+by (eres_inst_tac [("x", "Ts =>> T")] allE 1);
+by (eres_inst_tac [("x", "a[u/i]")] allE 1);
+by (eres_inst_tac [("x", "0")] allE 1);
+by (etac impE 1);
+by (Simp_tac 1);
+by (rtac typing.APP 1);
+by (subgoal_tac "(%j. if j = 0 then Ta else e (j - 1)) =  \
+ \  (%j. if j < 0 then e j else if j = 0 then Ta else e (j - 1))" 1);
+byev [etac ssubst 1, rtac lift_type' 1];
+by (assume_tac 1);
+by (rtac ext 1);
+by (case_tac "j" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (rtac typing.VAR 1);
+by (Simp_tac 1);
+by (fast_tac (claset() addSIs [subst_lemma]) 1);
+(** n~=i **)
+by (dtac list_app_typeD 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (dtac lists_types 1);
+by (subgoal_tac "map (%x. x[u/i]) rs : lists IT" 1);
+by (asm_simp_tac (simpset() addsimps [subst_Var]) 1);
+by (Fast_tac 1);
+by (etac (lists_IntI RS lists.induct) 1);
+by (assume_tac 1);
+by (fast_tac (claset() addss simpset()) 1);
+by (fast_tac (claset() addss simpset()) 1);
+(** Lambda **)
+by (fast_tac (claset() addss simpset()) 1);
+(** Beta **)
+by (strip_tac 1);
+by (Simp_tac 1);
+by (rtac IT.BetaI 1);
+by (simp_tac (simpset() delsimps [subst_map]
+  addsimps [subst_subst, subst_map RS sym]) 1);
+by (dtac subject_reduction 1);
+by (rtac apps_preserves_beta 1);
+by (rtac beta.beta 1);
+by (Fast_tac 1);
+by (dtac list_app_typeD 1);
+by (Fast_tac 1);
+qed_spec_mp "subst_type_IT";
+
+(**** main theorem: well-typed terms are strongly normalizing ****)
+
+Goal "e |- t : T ==> t : IT";
+by (etac typing.induct 1);
+by (rtac Var_IT 1);
+by (etac IT.LambdaI 1);
+by (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT" 1);
+by (Asm_full_simp_tac 1);
+by (rtac subst_type_IT 1);
+by (rtac (rewrite_rule (map mk_meta_eq [foldl_Nil, foldl_Cons])
+  (lists.Nil RSN (2, lists.Cons RS IT.VarI))) 1);
+by (etac lift_IT 1);
+by (rtac typing.APP 1);
+by (rtac typing.VAR 1);
+by (Simp_tac 1);
+by (etac lift_type' 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "type_implies_IT";
+
+bind_thm ("type_implies_termi", type_implies_IT RS IT_implies_termi);
diff -r e221d4f81d52 -r de99e37effda src/HOL/Lambda/Type.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/Type.thy	Fri Jun 23 12:24:37 2000 +0200
@@ -0,0 +1,40 @@
+(*  Title:      HOL/Lambda/Type.thy
+    ID:         $Id$
+    Author:     Stefan Berghofer
+    Copyright   2000 TU Muenchen
+
+Simply-typed lambda terms.
+*)
+
+Type = InductTermi +
+
+datatype typ = Atom nat
+             | Fun typ typ (infixr "=>" 200)
+
+consts
+  typing :: "((nat => typ) * dB * typ) set"
+
+syntax
+  "@type" :: "[nat => typ, dB, typ] => bool" ("_ |- _ : _" [50,50,50] 50)
+  "=>>"   :: "[typ list, typ] => typ" (infixl 150)
+
+translations
+  "env |- t : T" == "(env, t, T) : typing"
+  "Ts =>> T" == "foldr Fun Ts T"
+
+inductive typing
+intrs
+  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"
+
+consts
+  "types" :: "[nat => typ, dB list, typ list] => bool"
+
+primrec
+  "types e [] Ts = (Ts = [])"
+  "types e (t # ts) Ts = (case Ts of
+      [] => False
+    | T # Ts => e |- t : T & types e ts Ts)"
+
+end