intros;
authorwenzelm
Mon Aug 14 18:13:14 2000 +0200 (2000-08-14)
changeset 95966d6bf351b2cc
parent 9595 ec388b0a4eaa
child 9597 938a99cc55f7
intros;
src/HOL/Induct/Acc.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Isar_examples/W_correct.thy
src/HOL/Lambda/T.thy
     1.1 --- a/src/HOL/Induct/Acc.thy	Mon Aug 14 18:08:26 2000 +0200
     1.2 +++ b/src/HOL/Induct/Acc.thy	Mon Aug 14 18:13:14 2000 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *}
     1.5  
     1.6  inductive "acc r"
     1.7 -  intrs
     1.8 +  intros
     1.9      accI [rulify_prems]:
    1.10        "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
    1.11  
     2.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Mon Aug 14 18:08:26 2000 +0200
     2.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Mon Aug 14 18:13:14 2000 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4    tiling :: "'a set set => 'a set set";
     2.5  
     2.6  inductive "tiling A"
     2.7 -  intrs
     2.8 +  intros
     2.9      empty: "{} : tiling A"
    2.10      Un:    "a : A ==> t : tiling A ==> a <= - t
    2.11                ==> a Un t : tiling A";
    2.12 @@ -115,7 +115,7 @@
    2.13    domino  :: "(nat * nat) set set";
    2.14  
    2.15  inductive domino
    2.16 -  intrs
    2.17 +  intros
    2.18      horiz:  "{(i, j), (i, j + 1)} : domino"
    2.19      vertl:  "{(i, j), (i + 1, j)} : domino";
    2.20  
    2.21 @@ -179,8 +179,8 @@
    2.22  lemma domino_finite: "d: domino ==> finite d";
    2.23  proof (induct set: domino);
    2.24    fix i j :: nat;
    2.25 -  show "finite {(i, j), (i, j + 1)}"; by (intro Finites.intrs);
    2.26 -  show "finite {(i, j), (i + 1, j)}"; by (intro Finites.intrs);
    2.27 +  show "finite {(i, j), (i, j + 1)}"; by (intro Finites.intros);
    2.28 +  show "finite {(i, j), (i + 1, j)}"; by (intro Finites.intros);
    2.29  qed;
    2.30  
    2.31  
     3.1 --- a/src/HOL/Isar_examples/W_correct.thy	Mon Aug 14 18:08:26 2000 +0200
     3.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Mon Aug 14 18:13:14 2000 +0200
     3.3 @@ -33,7 +33,7 @@
     3.4    "a |- e :: t" == "(a,e,t) : has_type";
     3.5  
     3.6  inductive has_type
     3.7 -  intrs [simp]
     3.8 +  intros [simp]
     3.9      Var: "n < length a ==> a |- Var n :: a ! n"
    3.10      Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
    3.11      App: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Lambda/T.thy	Mon Aug 14 18:13:14 2000 +0200
     4.3 @@ -0,0 +1,472 @@
     4.4 +(*  Title:      HOL/Lambda/Type.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Stefan Berghofer
     4.7 +    Copyright   2000 TU Muenchen
     4.8 +
     4.9 +Simply-typed lambda terms.  Subject reduction and strong normalization
    4.10 +of simply-typed lambda terms.  Partly based on a paper proof by Ralph
    4.11 +Matthes.
    4.12 +*)
    4.13 +
    4.14 +theory Type = InductTermi:
    4.15 +
    4.16 +datatype type =
    4.17 +    Atom nat
    4.18 +  | Fun type type     (infixr "=>" 200)
    4.19 +
    4.20 +consts
    4.21 +  typing :: "((nat => type) * dB * type) set"
    4.22 +
    4.23 +syntax
    4.24 +  "_typing" :: "[nat => type, dB, type] => bool"   ("_ |- _ : _" [50,50,50] 50)
    4.25 +  "_funs"   :: "[type list, type] => type"         (infixl "=>>" 150)
    4.26 +
    4.27 +translations
    4.28 +  "env |- t : T" == "(env, t, T) : typing"
    4.29 +  "Ts =>> T" == "foldr Fun Ts T"
    4.30 +
    4.31 +declare IT.intros [intro!]     (* FIXME *)
    4.32 +
    4.33 +inductive typing
    4.34 +intros [intro!]
    4.35 +  Var: "env x = T ==> env |- Var x : T"
    4.36 +  Abs: "(nat_case T env) |- t : U ==> env |- (Abs t) : (T => U)"
    4.37 +  App: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"
    4.38 +
    4.39 +consts
    4.40 +  "types" :: "[nat => type, dB list, type list] => bool"
    4.41 +primrec
    4.42 +  "types e [] Ts = (Ts = [])"
    4.43 +  "types e (t # ts) Ts =
    4.44 +    (case Ts of
    4.45 +      [] => False
    4.46 +    | T # Ts => e |- t : T & types e ts Ts)"
    4.47 +
    4.48 +inductive_cases [elim!] =
    4.49 +  "e |- Var i : T"
    4.50 +  "e |- t $ u : T"
    4.51 +  "e |- Abs t : T"
    4.52 +
    4.53 +inductive_cases [elim!] =
    4.54 +  "x # xs : lists S"
    4.55 +
    4.56 +
    4.57 +text {* Some tests. *}
    4.58 +
    4.59 +lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : T \<and> U = T"
    4.60 +  apply (intro exI conjI)
    4.61 +  apply force
    4.62 +  apply (rule refl)
    4.63 +  done
    4.64 +
    4.65 +lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : T \<and> U = T";
    4.66 +  apply (intro exI conjI)
    4.67 +  apply force
    4.68 +  apply (rule refl)
    4.69 +  done
    4.70 +
    4.71 +
    4.72 +text {* n-ary function types *}
    4.73 +
    4.74 +lemma list_app_typeD [rulify]:
    4.75 +    "\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)"
    4.76 +  apply (induct_tac ts)
    4.77 +   apply simp
    4.78 +  apply (intro strip)
    4.79 +  apply simp
    4.80 +  apply (erule_tac x = "t $ a" in allE)
    4.81 +  apply (erule_tac x = T in allE)
    4.82 +  apply (erule impE)
    4.83 +   apply assumption
    4.84 +  apply (elim exE conjE)
    4.85 +  apply (mk_cases_tac "e |- t $ u : T")
    4.86 +  apply (rule_tac x = "Ta # Ts" in exI)
    4.87 +  apply simp
    4.88 +  done
    4.89 +
    4.90 +lemma list_app_typeI [rulify]:
    4.91 +  "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
    4.92 +  apply (induct_tac ts)
    4.93 +   apply (intro strip)
    4.94 +   apply simp
    4.95 +  apply (intro strip)
    4.96 +  apply (case_tac Ts)
    4.97 +   apply simp
    4.98 +  apply simp
    4.99 +  apply (erule_tac x = "t $ a" in allE)
   4.100 +  apply (erule_tac x = T in allE)
   4.101 +  apply (erule_tac x = lista in allE)
   4.102 +  apply (erule impE)
   4.103 +   apply (erule conjE)
   4.104 +   apply (erule typing.App)
   4.105 +   apply assumption
   4.106 +  apply blast
   4.107 +  done
   4.108 +
   4.109 +lemma lists_types [rulify]:
   4.110 +    "\<forall>Ts. types e ts Ts --> ts : lists {t. \<exists>T. e |- t : T}"
   4.111 +  apply (induct_tac ts)
   4.112 +   apply (intro strip)
   4.113 +   apply (case_tac Ts)
   4.114 +     apply simp
   4.115 +     apply (rule lists.Nil)
   4.116 +    apply simp
   4.117 +  apply (intro strip)
   4.118 +  apply (case_tac Ts)
   4.119 +   apply simp
   4.120 +  apply simp
   4.121 +  apply (rule lists.Cons)
   4.122 +   apply blast
   4.123 +  apply blast
   4.124 +  done
   4.125 +
   4.126 +
   4.127 +text {* lifting preserves termination and well-typedness *}
   4.128 +
   4.129 +lemma lift_map [rulify, simp]:
   4.130 +    "\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
   4.131 +  apply (induct_tac ts)
   4.132 +  apply simp_all
   4.133 +  done
   4.134 +
   4.135 +lemma subst_map [rulify, simp]:
   4.136 +  "\<forall>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts"
   4.137 +  apply (induct_tac ts)
   4.138 +  apply simp_all
   4.139 +  done
   4.140 +
   4.141 +lemma lift_IT [rulify, intro!]:
   4.142 +    "t : IT ==> \<forall>i. lift t i : IT"
   4.143 +  apply (erule IT.induct)
   4.144 +    apply (rule allI)
   4.145 +    apply (simp (no_asm))
   4.146 +    apply (rule conjI)
   4.147 +     apply
   4.148 +      (rule impI,
   4.149 +       rule IT.VarI,
   4.150 +       erule lists.induct,
   4.151 +       simp (no_asm),
   4.152 +       rule lists.Nil,
   4.153 +       simp (no_asm),
   4.154 +       erule IntE,
   4.155 +       rule lists.Cons,
   4.156 +       blast,
   4.157 +       assumption)+
   4.158 +     apply auto
   4.159 +   done
   4.160 +
   4.161 +lemma lifts_IT [rulify]:
   4.162 +    "ts : lists IT --> map (\<lambda>t. lift t 0) ts : lists IT"
   4.163 +  apply (induct_tac ts)
   4.164 +   apply auto
   4.165 +  done     
   4.166 +
   4.167 +
   4.168 +lemma shift_env [simp]:
   4.169 + "nat_case T
   4.170 +    (\<lambda>j. if j < i then e j else if j = i then Ua else e (j - 1)) =
   4.171 +    (\<lambda>j. if j < Suc i then nat_case T e j else if j = Suc i then Ua
   4.172 +          else nat_case T e (j - 1))"
   4.173 +  apply (rule ext)
   4.174 +  apply (case_tac j)
   4.175 +   apply simp
   4.176 +  apply (case_tac nat)
   4.177 +  apply simp_all
   4.178 +  done
   4.179 +
   4.180 +lemma lift_type' [rulify]:
   4.181 +  "e |- t : T ==> \<forall>i U.
   4.182 +    (\<lambda>j. if j < i then e j
   4.183 +          else if j = i then U 
   4.184 +          else e (j - 1)) |- lift t i : T"
   4.185 +  apply (erule typing.induct)
   4.186 +    apply auto
   4.187 +  done
   4.188 +
   4.189 +
   4.190 +lemma lift_type [intro!]:
   4.191 +  "e |- t : T ==> nat_case U e |- lift t 0 : T"
   4.192 +  apply (subgoal_tac
   4.193 +    "nat_case U e =
   4.194 +      (\<lambda>j. if j < 0 then e j
   4.195 +            else if j = 0 then U else e (j - 1))")
   4.196 +   apply (erule ssubst)
   4.197 +   apply (erule lift_type')
   4.198 +  apply (rule ext)
   4.199 +  apply (case_tac j)
   4.200 +   apply simp_all
   4.201 +  done
   4.202 +
   4.203 +lemma lift_types:
   4.204 +  "\<forall>Ts. types e ts Ts -->
   4.205 +    types (\<lambda>j. if j < i then e j
   4.206 +                else if j = i then U
   4.207 +                else e (j - 1)) (map (\<lambda>t. lift t i) ts) Ts"
   4.208 +  apply (induct_tac ts)
   4.209 +   apply simp
   4.210 +  apply (intro strip)
   4.211 +  apply (case_tac Ts)
   4.212 +   apply simp_all
   4.213 +  apply (rule lift_type')
   4.214 +  apply (erule conjunct1)
   4.215 +  done
   4.216 +
   4.217 +
   4.218 +text {* substitution lemma *}
   4.219 +
   4.220 +lemma subst_lemma [rulify]:
   4.221 + "e |- t : T ==> \<forall>e' i U u.
   4.222 +    e = (\<lambda>j. if j < i then e' j
   4.223 +              else if j = i then U
   4.224 +              else e' (j-1)) -->
   4.225 +    e' |- u : U --> e' |- t[u/i] : T"
   4.226 +  apply (erule typing.induct)
   4.227 +    apply (intro strip)
   4.228 +    apply (case_tac "x = i")
   4.229 +     apply simp
   4.230 +    apply (frule linorder_neq_iff [RS iffD1])
   4.231 +    apply (erule disjE)
   4.232 +     apply simp
   4.233 +     apply (rule typing.Var)
   4.234 +     apply assumption
   4.235 +    apply (frule order_less_not_sym)
   4.236 +    apply (simp only: subst_gt split: split_if add: if_False)
   4.237 +    apply (rule typing.Var)
   4.238 +    apply assumption
   4.239 +   apply fastsimp
   4.240 +  apply fastsimp
   4.241 +  done
   4.242 +
   4.243 +lemma substs_lemma [rulify]:
   4.244 +  "e |- u : T ==>
   4.245 +    \<forall>Ts. types (\<lambda>j. if j < i then e j
   4.246 +                     else if j = i then T else e (j - 1)) ts Ts -->
   4.247 +      types e (map (%t. t[u/i]) ts) Ts"
   4.248 +  apply (induct_tac ts)
   4.249 +   apply (intro strip)
   4.250 +   apply (case_tac Ts)
   4.251 +    apply simp
   4.252 +   apply simp
   4.253 +  apply (intro strip)
   4.254 +  apply (case_tac Ts)
   4.255 +   apply simp
   4.256 +  apply simp
   4.257 +  apply (erule conjE)
   4.258 +  apply (erule subst_lemma)
   4.259 +  apply (rule refl)
   4.260 +  apply assumption
   4.261 +  done
   4.262 +
   4.263 +
   4.264 +text {* subject reduction *}
   4.265 +
   4.266 +lemma subject_reduction [rulify]:
   4.267 +    "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T"
   4.268 +  apply (erule typing.induct)
   4.269 +    apply blast
   4.270 +   apply blast
   4.271 +  apply (intro strip)
   4.272 +  apply (mk_cases_tac "s $ t -> t'")
   4.273 +    apply hyp_subst
   4.274 +    apply (mk_cases_tac "env |- Abs t : T => U")
   4.275 +    apply (rule subst_lemma)
   4.276 +      apply assumption
   4.277 +     prefer 2
   4.278 +     apply assumption
   4.279 +    apply (rule ext)
   4.280 +    apply (case_tac j)
   4.281 +     apply auto
   4.282 +  done
   4.283 +
   4.284 +text {* additional lemmas *}
   4.285 +
   4.286 +lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])"
   4.287 +  apply simp
   4.288 +  done
   4.289 +
   4.290 +
   4.291 +lemma subst_Var_IT [rulify]: "r : IT ==> \<forall>i j. r[Var i/j] : IT"
   4.292 +  apply (erule IT.induct)
   4.293 +    txt {* Var *}
   4.294 +    apply (intro strip)
   4.295 +    apply (simp (no_asm) add: subst_Var)
   4.296 +    apply
   4.297 +    ((rule conjI impI)+,
   4.298 +      rule IT.VarI,
   4.299 +      erule lists.induct,
   4.300 +      simp (no_asm),
   4.301 +      rule lists.Nil,
   4.302 +      simp (no_asm),
   4.303 +      erule IntE,
   4.304 +      erule CollectE,
   4.305 +      rule lists.Cons,
   4.306 +      fast,
   4.307 +      assumption)+
   4.308 +   txt {* Lambda *}
   4.309 +   apply (intro strip)
   4.310 +   apply simp
   4.311 +   apply (rule IT.LambdaI)
   4.312 +   apply fast
   4.313 +  txt {* Beta *}
   4.314 +  apply (intro strip)
   4.315 +  apply (simp (no_asm_use) add: subst_subst [RS sym])
   4.316 +  apply (rule IT.BetaI)
   4.317 +   apply auto
   4.318 +  done
   4.319 +
   4.320 +lemma Var_IT: "Var n \<in> IT"
   4.321 +proof -
   4.322 +  have "Var n $$ [] \<in> IT"
   4.323 +    apply (rule IT.VarI)
   4.324 +    apply (rule lists.Nil)
   4.325 +    done
   4.326 +  then show ?thesis by simp
   4.327 +qed
   4.328 +
   4.329 +
   4.330 +lemma app_Var_IT: "t : IT ==> t $ Var i : IT"
   4.331 +  apply (erule IT.induct)
   4.332 +    apply (subst app_last)
   4.333 +    apply (rule IT.VarI)
   4.334 +    apply simp
   4.335 +    apply (rule lists.Cons)
   4.336 +     apply (rule Var_IT)
   4.337 +    apply (rule lists.Nil)
   4.338 +   apply (rule IT.BetaI [where ?ss = "[]", unfold foldl_Nil [RS eq_reflection]])
   4.339 +    apply (erule subst_Var_IT)
   4.340 +   apply (rule Var_IT)
   4.341 +  apply (subst app_last)
   4.342 +  apply (rule IT.BetaI)
   4.343 +   apply (subst app_last [RS sym])
   4.344 +   apply assumption
   4.345 +  apply assumption
   4.346 +  done
   4.347 +
   4.348 +
   4.349 +text {* Well-typed substitution preserves termination. *}
   4.350 +
   4.351 +lemma subst_type_IT [rulify]:
   4.352 +  "\<forall>t. t : IT --> (\<forall>e T u i.
   4.353 +    (\<lambda>j. if j < i then e j
   4.354 +          else if j = i then U
   4.355 +          else e (j - 1)) |- t : T -->
   4.356 +    u : IT --> e |- u : U --> t[u/i] : IT)"
   4.357 +  apply (rule_tac f = size and a = U in measure_induct)
   4.358 +  apply (rule allI)
   4.359 +  apply (rule impI)
   4.360 +  apply (erule IT.induct)
   4.361 +    txt {* Var *}
   4.362 +    apply (intro strip)
   4.363 +    apply (case_tac "n = i")
   4.364 +     txt {* n=i *}
   4.365 +     apply (case_tac rs)
   4.366 +      apply simp
   4.367 +     apply simp
   4.368 +     apply (drule list_app_typeD)
   4.369 +     apply (elim exE conjE)
   4.370 +     apply (mk_cases_tac "e |- t $ u : T")
   4.371 +     apply (mk_cases_tac "e |- Var i : T")
   4.372 +     apply (drule_tac s = "(?T::type) => ?U" in sym)
   4.373 +     apply simp
   4.374 +     apply (subgoal_tac "lift u 0 $ Var 0 : IT")
   4.375 +      prefer 2
   4.376 +      apply (rule app_Var_IT)
   4.377 +      apply (erule lift_IT)
   4.378 +     apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] : IT")
   4.379 +      apply (simp (no_asm_use))
   4.380 +      apply (subgoal_tac "(Var 0 $$ map (%t. lift t 0)
   4.381 +        (map (%t. t[u/i]) list))[(u $ a[u/i])/0] : IT")
   4.382 +       apply (simp (no_asm_use) del: map_compose add: map_compose [RS sym] o_def)
   4.383 +      apply (erule_tac x = "Ts =>> T" in allE)
   4.384 +      apply (erule impE)
   4.385 +       apply simp
   4.386 +      apply (erule_tac x = "Var 0 $$
   4.387 +        map (%t. lift t 0) (map (%t. t[u/i]) list)" in allE)
   4.388 +      apply (erule impE)
   4.389 +       apply (rule IT.VarI)
   4.390 +       apply (rule lifts_IT)
   4.391 +       apply (drule lists_types)
   4.392 +       apply
   4.393 +        (mk_cases_tac "x # xs : lists (Collect P)",
   4.394 +	 erule lists_IntI [RS lists.induct],
   4.395 +	 assumption)
   4.396 +	apply fastsimp
   4.397 +       apply fastsimp
   4.398 +       apply (erule_tac x = e in allE)
   4.399 +       apply (erule_tac x = T in allE)
   4.400 +       apply (erule_tac x = "u $ a[u/i]" in allE)
   4.401 +       apply (erule_tac x = 0 in allE)
   4.402 +       apply (force intro!: lift_types list_app_typeI substs_lemma subst_lemma)
   4.403 +
   4.404 +by (eres_inst_tac [("x", "Ta")] allE 1);
   4.405 +by (etac impE 1);
   4.406 +by (Simp_tac 1);
   4.407 +by (eres_inst_tac [("x", "lift u 0 $ Var 0")] allE 1);
   4.408 +by (etac impE 1);
   4.409 +by (assume_tac 1);
   4.410 +by (eres_inst_tac [("x", "e")] allE 1);
   4.411 +by (eres_inst_tac [("x", "Ts =>> T")] allE 1);
   4.412 +by (eres_inst_tac [("x", "a[u/i]")] allE 1);
   4.413 +by (eres_inst_tac [("x", "0")] allE 1);
   4.414 +by (etac impE 1);
   4.415 +by (rtac typing.APP 1);
   4.416 +by (etac lift_type' 1);
   4.417 +by (rtac typing.VAR 1);
   4.418 +by (Simp_tac 1);
   4.419 +by (fast_tac (claset() addSIs [subst_lemma]) 1);
   4.420 +(** n~=i **)
   4.421 +by (dtac list_app_typeD 1);
   4.422 +by (etac exE 1);
   4.423 +by (etac conjE 1);
   4.424 +by (dtac lists_types 1);
   4.425 +by (subgoal_tac "map (%x. x[u/i]) rs : lists IT" 1);
   4.426 +by (asm_simp_tac (simpset() addsimps [subst_Var]) 1);
   4.427 +by (Fast_tac 1);
   4.428 +by (etac (lists_IntI RS lists.induct) 1);
   4.429 +by (assume_tac 1);
   4.430 +by (fast_tac (claset() addss simpset()) 1);
   4.431 +by (fast_tac (claset() addss simpset()) 1);
   4.432 +(** Lambda **)
   4.433 +by (fast_tac (claset() addss simpset()) 1);
   4.434 +(** Beta **)
   4.435 +by (strip_tac 1);
   4.436 +by (Simp_tac 1);
   4.437 +by (rtac IT.BetaI 1);
   4.438 +by (simp_tac (simpset() delsimps [subst_map]
   4.439 +  addsimps [subst_subst, subst_map RS sym]) 1);
   4.440 +by (dtac subject_reduction 1);
   4.441 +by (rtac apps_preserves_beta 1);
   4.442 +by (rtac beta.beta 1);
   4.443 +by (Fast_tac 1);
   4.444 +by (dtac list_app_typeD 1);
   4.445 +by (Fast_tac 1);
   4.446 +qed_spec_mp "subst_type_IT";
   4.447 +
   4.448 +done
   4.449 +
   4.450 +
   4.451 +
   4.452 +
   4.453 +
   4.454 +(**** main theorem: well-typed terms are strongly normalizing ****)
   4.455 +
   4.456 +Goal "e |- t : T ==> t : IT";
   4.457 +by (etac typing.induct 1);
   4.458 +by (rtac Var_IT 1);
   4.459 +by (etac IT.LambdaI 1);
   4.460 +by (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT" 1);
   4.461 +by (Asm_full_simp_tac 1);
   4.462 +by (rtac subst_type_IT 1);
   4.463 +by (rtac (rewrite_rule (map mk_meta_eq [foldl_Nil, foldl_Cons])
   4.464 +  (lists.Nil RSN (2, lists.Cons RS IT.VarI))) 1);
   4.465 +by (etac lift_IT 1);
   4.466 +by (rtac typing.APP 1);
   4.467 +by (rtac typing.VAR 1);
   4.468 +by (Simp_tac 1);
   4.469 +by (etac lift_type' 1);
   4.470 +by (assume_tac 1);
   4.471 +by (assume_tac 1);
   4.472 +qed "type_implies_IT";
   4.473 +
   4.474 +bind_thm ("type_implies_termi", type_implies_IT RS IT_implies_termi);
   4.475 +