# HG changeset patch
# User wenzelm
# Date 966522230 -7200
# Node ID 1f62547edc0e14755cc47722092196e7b4af639f
# Parent  47d39a31eb2f6bf0a7f3d9c61daee7e3d7705fcc
removed Lambda/Type.ML;

diff -r 47d39a31eb2f -r 1f62547edc0e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Aug 17 12:02:01 2000 +0200
+++ b/src/HOL/IsaMakefile	Thu Aug 17 16:23:50 2000 +0200
@@ -308,8 +308,7 @@
   Lambda/InductTermi.thy Lambda/Lambda.ML Lambda/Lambda.thy \
   Lambda/ListApplication.ML Lambda/ListApplication.thy Lambda/ListBeta.ML \
   Lambda/ListBeta.thy Lambda/ListOrder.ML Lambda/ListOrder.thy \
-  Lambda/ParRed.ML Lambda/ParRed.thy Lambda/Type.ML Lambda/Type.thy \
-  Lambda/ROOT.ML
+  Lambda/ParRed.ML Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Lambda
 
 
diff -r 47d39a31eb2f -r 1f62547edc0e src/HOL/Lambda/Type.ML
--- a/src/HOL/Lambda/Type.ML	Thu Aug 17 12:02:01 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,403 +0,0 @@
-(*  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 "(t $$ ts) $ u = t $$ (ts @ [u])";
-by (Simp_tac 1);
-qed "app_last";
-
-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";
-
-bind_thm ("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 (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 (rtac typing.APP 1);
-by (etac lift_type' 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);