src/HOL/MiniML/Type.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4502 337c073de95e
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (* Title:     HOL/MiniML/Type.thy
     2    ID:        $Id$
     3    Author:    Wolfgang Naraschewski and Tobias Nipkow
     4    Copyright  1996 TU Muenchen
     5 *)
     6 
     7 Addsimps [mgu_eq,mgu_mg,mgu_free];
     8 
     9 
    10 (* lemmata for make scheme *)
    11 
    12 goal thy "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)";
    13 by (typ.induct_tac "t" 1);
    14 by (Simp_tac 1);
    15 by (Asm_full_simp_tac 1);
    16 by (Fast_tac 1);
    17 qed_spec_mp "mk_scheme_Fun";
    18 
    19 goal thy "!t'. mk_scheme t = mk_scheme t' --> t=t'";
    20 by (typ.induct_tac "t" 1);
    21  by (rtac allI 1);
    22  by (typ.induct_tac "t'" 1);
    23   by (Simp_tac 1);
    24  by (Asm_full_simp_tac 1);
    25 by (rtac allI 1);
    26 by (typ.induct_tac "t'" 1);
    27  by (Simp_tac 1);
    28 by (Asm_full_simp_tac 1);
    29 qed_spec_mp "mk_scheme_injective";
    30 
    31 goal thy "!!t. free_tv (mk_scheme t) = free_tv t";
    32 by (typ.induct_tac "t" 1);
    33 by (ALLGOALS Asm_simp_tac);
    34 qed "free_tv_mk_scheme";
    35 
    36 Addsimps [free_tv_mk_scheme];
    37 
    38 goal thy "!!t. $ S (mk_scheme t) = mk_scheme ($ S t)";
    39 by (typ.induct_tac "t" 1);
    40 by (ALLGOALS Asm_simp_tac);
    41 qed "subst_mk_scheme";
    42 
    43 Addsimps [subst_mk_scheme];
    44 
    45 
    46 (* constructor laws for app_subst *)
    47 
    48 goalw thy [app_subst_list]
    49   "$ S [] = []";
    50 by (Simp_tac 1);
    51 qed "app_subst_Nil";
    52 
    53 goalw thy [app_subst_list]
    54   "$ S (x#l) = ($ S x)#($ S l)";
    55 by (Simp_tac 1);
    56 qed "app_subst_Cons";
    57 
    58 Addsimps [app_subst_Nil,app_subst_Cons];
    59 
    60 
    61 (* constructor laws for new_tv *)
    62 
    63 goalw thy [new_tv_def]
    64   "new_tv n (TVar m) = (m<n)";
    65 by (fast_tac (HOL_cs addss simpset()) 1);
    66 qed "new_tv_TVar";
    67 
    68 goalw thy [new_tv_def]
    69   "new_tv n (FVar m) = (m<n)";
    70 by (fast_tac (HOL_cs addss simpset()) 1);
    71 qed "new_tv_FVar";
    72 
    73 goalw thy [new_tv_def]
    74   "new_tv n (BVar m) = True";
    75 by (Simp_tac 1);
    76 qed "new_tv_BVar";
    77 
    78 goalw thy [new_tv_def]
    79   "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)";
    80 by (fast_tac (HOL_cs addss simpset()) 1);
    81 qed "new_tv_Fun";
    82 
    83 goalw thy [new_tv_def]
    84   "new_tv n (t1 =-> t2) = (new_tv n t1 & new_tv n t2)";
    85 by (fast_tac (HOL_cs addss simpset()) 1);
    86 qed "new_tv_Fun2";
    87 
    88 goalw thy [new_tv_def]
    89   "new_tv n []";
    90 by (Simp_tac 1);
    91 qed "new_tv_Nil";
    92 
    93 goalw thy [new_tv_def]
    94   "new_tv n (x#l) = (new_tv n x & new_tv n l)";
    95 by (fast_tac (HOL_cs addss simpset()) 1);
    96 qed "new_tv_Cons";
    97 
    98 goalw thy [new_tv_def] "!!n. new_tv n TVar";
    99 by (strip_tac 1);
   100 by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1);
   101 qed "new_tv_TVar_subst";
   102 
   103 Addsimps [new_tv_TVar,new_tv_FVar,new_tv_BVar,new_tv_Fun,new_tv_Fun2,new_tv_Nil,new_tv_Cons,new_tv_TVar_subst];
   104 
   105 goalw thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
   106   "new_tv n id_subst";
   107 by (Simp_tac 1);
   108 qed "new_tv_id_subst";
   109 Addsimps[new_tv_id_subst];
   110 
   111 goal thy "new_tv n (sch::type_scheme) --> \
   112 \              $(%k. if k<n then S k else S' k) sch = $S sch";
   113 by (type_scheme.induct_tac "sch" 1);
   114 by (ALLGOALS Asm_simp_tac);
   115 qed "new_if_subst_type_scheme";
   116 Addsimps [new_if_subst_type_scheme];
   117 
   118 goal thy "new_tv n (A::type_scheme list) --> \
   119 \              $(%k. if k<n then S k else S' k) A = $S A";
   120 by (list.induct_tac "A" 1);
   121 by (ALLGOALS Asm_simp_tac);
   122 qed "new_if_subst_type_scheme_list";
   123 Addsimps [new_if_subst_type_scheme_list];
   124 
   125 
   126 (* constructor laws for dom and cod *)
   127 
   128 goalw thy [dom_def,id_subst_def,empty_def]
   129   "dom id_subst = {}";
   130 by (Simp_tac 1);
   131 qed "dom_id_subst";
   132 Addsimps [dom_id_subst];
   133 
   134 goalw thy [cod_def]
   135   "cod id_subst = {}";
   136 by (Simp_tac 1);
   137 qed "cod_id_subst";
   138 Addsimps [cod_id_subst];
   139 
   140 
   141 (* lemmata for free_tv *)
   142 
   143 goalw thy [free_tv_subst]
   144   "free_tv id_subst = {}";
   145 by (Simp_tac 1);
   146 qed "free_tv_id_subst";
   147 Addsimps [free_tv_id_subst];
   148 
   149 goal thy "!!A. !n. n < length A --> x : free_tv (nth n A) --> x : free_tv A";
   150 by (list.induct_tac "A" 1);
   151 by (Asm_full_simp_tac 1);
   152 by (rtac allI 1);
   153 by (res_inst_tac [("n","n")] nat_induct 1);
   154 by (Asm_full_simp_tac 1);
   155 by (Asm_full_simp_tac 1);
   156 qed_spec_mp "free_tv_nth_A_impl_free_tv_A";
   157 
   158 Addsimps [free_tv_nth_A_impl_free_tv_A];
   159 
   160 goal thy "!!A. !nat. nat < length A --> x : free_tv (nth nat A) --> x : free_tv A";
   161 by (list.induct_tac "A" 1);
   162 by (Asm_full_simp_tac 1);
   163 by (rtac allI 1);
   164 by (res_inst_tac [("n","nat")] nat_induct 1);
   165 by (strip_tac 1);
   166 by (Asm_full_simp_tac 1);
   167 by (Simp_tac 1);
   168 qed_spec_mp "free_tv_nth_nat_A";
   169 
   170 
   171 (* if two substitutions yield the same result if applied to a type
   172    structure the substitutions coincide on the free type variables
   173    occurring in the type structure *)
   174 
   175 goal thy "!!S S'. (!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t";
   176 by (typ.induct_tac "t" 1);
   177 by (Simp_tac 1);
   178 by (Asm_full_simp_tac 1);
   179 qed_spec_mp "typ_substitutions_only_on_free_variables";
   180 
   181 goal thy
   182   "!!t. (!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t";
   183 by (rtac typ_substitutions_only_on_free_variables 1);
   184 by (simp_tac (simpset() addsimps [Ball_def]) 1);
   185 qed "eq_free_eq_subst_te";
   186 
   187 goal thy "!!S S'. (!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch";
   188 by (type_scheme.induct_tac "sch" 1);
   189 by (Simp_tac 1);
   190 by (Simp_tac 1);
   191 by (Asm_full_simp_tac 1);
   192 qed_spec_mp "scheme_substitutions_only_on_free_variables";
   193 
   194 goal thy
   195   "!!sch. (!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch";
   196 by (rtac scheme_substitutions_only_on_free_variables 1);
   197 by (simp_tac (simpset() addsimps [Ball_def]) 1);
   198 qed "eq_free_eq_subst_type_scheme";
   199 
   200 goal thy
   201   "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A";
   202 by (list.induct_tac "A" 1); 
   203 (* case [] *)
   204 by (fast_tac (HOL_cs addss simpset()) 1);
   205 (* case x#xl *)
   206 by (fast_tac (HOL_cs addIs [eq_free_eq_subst_type_scheme] addss (simpset())) 1);
   207 qed_spec_mp "eq_free_eq_subst_scheme_list";
   208 
   209 goal thy "!!P Q. ((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)";
   210 by (Fast_tac 1);
   211 val weaken_asm_Un = result ();
   212 
   213 goal thy "!!S S'. (!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A";
   214 by (list.induct_tac "A" 1);
   215 by (Simp_tac 1);
   216 by (Asm_full_simp_tac 1);
   217 by (rtac weaken_asm_Un 1);
   218 by (strip_tac 1);
   219 by (etac scheme_substitutions_only_on_free_variables 1);
   220 qed_spec_mp "scheme_list_substitutions_only_on_free_variables";
   221 
   222 goal thy
   223   "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n";
   224 by (typ.induct_tac "t" 1);
   225 (* case TVar n *)
   226 by (fast_tac (HOL_cs addss simpset()) 1);
   227 (* case Fun t1 t2 *)
   228 by (fast_tac (HOL_cs addss simpset()) 1);
   229 qed_spec_mp "eq_subst_te_eq_free";
   230 
   231 goal thy
   232   "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n";
   233 by (type_scheme.induct_tac "sch" 1);
   234 (* case TVar n *)
   235 by (Asm_simp_tac 1);
   236 (* case BVar n *)
   237 by (strip_tac 1);
   238 by (etac mk_scheme_injective 1);
   239 by (Asm_simp_tac 1);
   240 (* case Fun t1 t2 *)
   241 by (Asm_full_simp_tac 1);
   242 qed_spec_mp "eq_subst_type_scheme_eq_free";
   243 
   244 goal thy
   245   "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n";
   246 by (list.induct_tac "A" 1);
   247 (* case [] *)
   248 by (fast_tac (HOL_cs addss simpset()) 1);
   249 (* case x#xl *)
   250 by (fast_tac (HOL_cs addIs [eq_subst_type_scheme_eq_free] addss (simpset())) 1);
   251 qed_spec_mp "eq_subst_scheme_list_eq_free";
   252 
   253 goalw thy [free_tv_subst] 
   254       "!!v. v : cod S ==> v : free_tv S";
   255 by (fast_tac set_cs 1);
   256 qed "codD";
   257  
   258 goalw thy [free_tv_subst,dom_def] 
   259       "!! x. x ~: free_tv S ==> S x = TVar x";
   260 by (fast_tac set_cs 1);
   261 qed "not_free_impl_id";
   262 
   263 goalw thy [new_tv_def] 
   264       "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
   265 by (fast_tac HOL_cs 1 );
   266 qed "free_tv_le_new_tv";
   267 
   268 goalw thy [dom_def,cod_def,UNION_def,Bex_def]
   269   "!!v. [| v : free_tv(S n); v~=n |] ==> v : cod S";
   270 by (Simp_tac 1);
   271 by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
   272 by (assume_tac 2);
   273 by (rotate_tac 1 1);
   274 by (Asm_full_simp_tac 1);
   275 qed "cod_app_subst";
   276 Addsimps [cod_app_subst];
   277 
   278 goal thy 
   279      "free_tv (S (v::nat)) <= insert v (cod S)";
   280 by (expand_case_tac "v:dom S" 1);
   281 by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1);
   282 by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1);
   283 qed "free_tv_subst_var";
   284 
   285 goal thy 
   286      "free_tv ($ S (t::typ)) <= cod S Un free_tv t";
   287 by (typ.induct_tac "t" 1);
   288 (* case TVar n *)
   289 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
   290 (* case Fun t1 t2 *)
   291 by (fast_tac (set_cs addss simpset()) 1);
   292 qed "free_tv_app_subst_te";     
   293 
   294 goal thy 
   295      "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
   296 by (type_scheme.induct_tac "sch" 1);
   297 (* case FVar n *)
   298 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
   299 (* case BVar n *)
   300 by (Simp_tac 1);
   301 (* case Fun t1 t2 *)
   302 by (fast_tac (set_cs addss simpset()) 1);
   303 qed "free_tv_app_subst_type_scheme";  
   304 
   305 goal thy 
   306      "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
   307 by (list.induct_tac "A" 1);
   308 (* case [] *)
   309 by (Simp_tac 1);
   310 (* case a#al *)
   311 by (cut_facts_tac [free_tv_app_subst_type_scheme] 1);
   312 by (fast_tac (set_cs addss simpset()) 1);
   313 qed "free_tv_app_subst_scheme_list";
   314 
   315 goalw thy [free_tv_subst,dom_def]
   316      "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=   \
   317 \     free_tv s1 Un free_tv s2";
   318 by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,
   319                              free_tv_subst_var RS subsetD] 
   320                      addss (simpset() delsimps bex_simps
   321                                      addsimps [cod_def,dom_def])) 1);
   322 qed "free_tv_comp_subst";
   323 
   324 goalw thy [o_def] 
   325      "free_tv ($ S1 o S2) <= free_tv S1 Un free_tv (S2 :: nat => typ)";
   326 by (rtac free_tv_comp_subst 1);
   327 qed "free_tv_o_subst";
   328 
   329 goal thy "!!n. n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)";
   330 by (typ.induct_tac "t" 1);
   331 by (Simp_tac 1);
   332 by (Simp_tac 1);
   333 by (Fast_tac 1);
   334 qed_spec_mp "free_tv_of_substitutions_extend_to_types";
   335 
   336 goal thy "!!n. n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)";
   337 by (type_scheme.induct_tac "sch" 1);
   338 by (Simp_tac 1);
   339 by (Simp_tac 1);
   340 by (Simp_tac 1);
   341 by (Fast_tac 1);
   342 qed_spec_mp "free_tv_of_substitutions_extend_to_schemes";
   343 
   344 goal thy "!!n. n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)";
   345 by (list.induct_tac "A" 1);
   346 by (Simp_tac 1);
   347 by (Simp_tac 1);
   348 by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_schemes]) 1);
   349 qed_spec_mp "free_tv_of_substitutions_extend_to_scheme_lists";
   350 
   351 Addsimps [free_tv_of_substitutions_extend_to_scheme_lists];
   352 
   353 goal thy "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
   354 by (type_scheme.induct_tac "sch" 1);
   355 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   356 by (strip_tac 1);
   357 by (Fast_tac 1);
   358 qed "free_tv_ML_scheme";
   359 
   360 goal thy "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
   361 by (list.induct_tac "A" 1);
   362 by (Simp_tac 1);
   363 by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme]) 1);
   364 qed "free_tv_ML_scheme_list";
   365 
   366 
   367 (* lemmata for bound_tv *)
   368 
   369 goal thy "!!t. bound_tv (mk_scheme t) = {}";
   370 by (typ.induct_tac "t" 1);
   371 by (ALLGOALS Asm_simp_tac);
   372 qed "bound_tv_mk_scheme";
   373 
   374 Addsimps [bound_tv_mk_scheme];
   375 
   376 goal thy "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch";
   377 by (type_scheme.induct_tac "sch" 1);
   378 by (ALLGOALS Asm_simp_tac);
   379 qed "bound_tv_subst_scheme";
   380 
   381 Addsimps [bound_tv_subst_scheme];
   382 
   383 goal thy "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A";
   384 by (rtac list.induct 1);
   385 by (Simp_tac 1);
   386 by (Asm_simp_tac 1);
   387 qed "bound_tv_subst_scheme_list";
   388 
   389 Addsimps [bound_tv_subst_scheme_list];
   390 
   391 
   392 (* lemmata for new_tv *)
   393 
   394 goalw thy [new_tv_def]
   395   "new_tv n S = ((!m. n <= m --> (S m = TVar m)) & \
   396 \                (! l. l < n --> new_tv n (S l) ))";
   397 by (safe_tac HOL_cs );
   398 (* ==> *)
   399 by (fast_tac (HOL_cs addDs [leD] addss (simpset() addsimps [free_tv_subst,dom_def])) 1);
   400 by (subgoal_tac "m:cod S | S l = TVar l" 1);
   401 by (safe_tac HOL_cs );
   402 by (fast_tac (HOL_cs addDs [UnI2] addss (simpset() addsimps [free_tv_subst])) 1);
   403 by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
   404 by (Asm_full_simp_tac 1);
   405 by (fast_tac (set_cs addss (simpset() addsimps [free_tv_subst,cod_def,dom_def])) 1);
   406 (* <== *)
   407 by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
   408 by (safe_tac set_cs );
   409 by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
   410 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   411 by (cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
   412 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   413 qed "new_tv_subst";
   414 
   415 goal thy 
   416   "new_tv n  = list_all (new_tv n)";
   417 by (rtac ext 1);
   418 by (list.induct_tac "x" 1);
   419 by (ALLGOALS Asm_simp_tac);
   420 qed "new_tv_list";
   421 
   422 (* substitution affects only variables occurring freely *)
   423 goal thy
   424   "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
   425 by (typ.induct_tac "t" 1);
   426 by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   427 qed "subst_te_new_tv";
   428 Addsimps [subst_te_new_tv];
   429 
   430 goal thy
   431   "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
   432 by (type_scheme.induct_tac "sch" 1);
   433 by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   434 qed_spec_mp "subst_te_new_type_scheme";
   435 Addsimps [subst_te_new_type_scheme];
   436 
   437 goal thy
   438   "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A";
   439 by (list.induct_tac "A" 1);
   440 by (ALLGOALS Asm_full_simp_tac);
   441 qed_spec_mp "subst_tel_new_scheme_list";
   442 Addsimps [subst_tel_new_scheme_list];
   443 
   444 (* all greater variables are also new *)
   445 goalw thy [new_tv_def] 
   446   "!!n m. n<=m ==> new_tv n t ==> new_tv m t";
   447 by Safe_tac;
   448 by (dtac spec 1);
   449 by (mp_tac 1);
   450 by (trans_tac 1);
   451 qed "new_tv_le";
   452 Addsimps [lessI RS less_imp_le RS new_tv_le];
   453 
   454 goal thy "!!n m. n<=m ==> new_tv n (t::typ) ==> new_tv m t";
   455 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
   456 qed "new_tv_typ_le";
   457 
   458 goal thy "!!n m. n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A";
   459 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
   460 qed "new_scheme_list_le";
   461 
   462 goal thy "!!n m. n<=m ==> new_tv n (S::subst) ==> new_tv m S";
   463 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
   464 qed "new_tv_subst_le";
   465 
   466 (* new_tv property remains if a substitution is applied *)
   467 goal thy
   468   "!!n. [| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)";
   469 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   470 qed "new_tv_subst_var";
   471 
   472 goal thy
   473   "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)";
   474 by (typ.induct_tac "t" 1);
   475 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
   476 qed_spec_mp "new_tv_subst_te";
   477 Addsimps [new_tv_subst_te];
   478 
   479 goal thy "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)";
   480 by (type_scheme.induct_tac "sch" 1);
   481 by (ALLGOALS (Asm_full_simp_tac));
   482 by (rewtac new_tv_def);
   483 by (simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1);
   484 by (strip_tac 1);
   485 by (case_tac "S nat = TVar nat" 1);
   486 by (rotate_tac 3 1);
   487 by (Asm_full_simp_tac 1);
   488 by (dres_inst_tac [("x","m")] spec 1);
   489 by (Fast_tac 1);
   490 qed_spec_mp "new_tv_subst_type_scheme";
   491 Addsimps [new_tv_subst_type_scheme];
   492 
   493 goal thy
   494   "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)";
   495 by (list.induct_tac "A" 1);
   496 by (ALLGOALS(fast_tac (HOL_cs addss (simpset()))));
   497 qed_spec_mp "new_tv_subst_scheme_list";
   498 Addsimps [new_tv_subst_scheme_list];
   499 
   500 goal thy
   501   "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
   502 by (simp_tac (simpset() addsimps [new_tv_list]) 1);
   503 by (list.induct_tac "A" 1);
   504 by (ALLGOALS Asm_full_simp_tac);
   505 qed "new_tv_Suc_list";
   506 
   507 goalw thy [new_tv_def] "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')";
   508 by (Asm_simp_tac 1);
   509 qed_spec_mp "new_tv_only_depends_on_free_tv_type_scheme";
   510 
   511 goalw thy [new_tv_def] "!!A::type_scheme list. (free_tv A) = (free_tv A') --> (new_tv n A --> new_tv n A')";
   512 by (Asm_simp_tac 1);
   513 qed_spec_mp "new_tv_only_depends_on_free_tv_scheme_list";
   514 
   515 goalw thy [new_tv_def] "!!A. !nat. nat < length A --> new_tv n A --> (new_tv n (nth nat A))";
   516 by (list.induct_tac "A" 1);
   517 by (Asm_full_simp_tac 1);
   518 by (rtac allI 1);
   519 by (res_inst_tac [("n","nat")] nat_induct 1);
   520 by (strip_tac 1);
   521 by (Asm_full_simp_tac 1);
   522 by (Simp_tac 1);
   523 qed_spec_mp "new_tv_nth_nat_A";
   524 
   525 
   526 (* composition of substitutions preserves new_tv proposition *)
   527 goal thy 
   528      "!! n. [| new_tv n (S::subst); new_tv n R |] ==> \
   529 \           new_tv n (($ R) o S)";
   530 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   531 qed "new_tv_subst_comp_1";
   532 
   533 goal thy
   534      "!! n. [| new_tv n (S::subst); new_tv n R |] ==>  \ 
   535 \     new_tv n (%v.$ R (S v))";
   536 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   537 qed "new_tv_subst_comp_2";
   538 
   539 Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2];
   540 
   541 (* new type variables do not occur freely in a type structure *)
   542 goalw thy [new_tv_def] 
   543       "!!n. new_tv n A ==> n~:(free_tv A)";
   544 by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
   545 qed "new_tv_not_free_tv";
   546 Addsimps [new_tv_not_free_tv];
   547 
   548 goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
   549 by (simp_tac (simpset() addsplits [expand_if]) 1);
   550 by Safe_tac;
   551 by (trans_tac 1);
   552 qed "less_maxL";
   553 
   554 goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
   555 by (simp_tac (simpset() addsplits [expand_if]) 1);
   556 by (fast_tac (claset() addDs [not_leE] addIs [less_trans]) 1);
   557 val less_maxR = result();
   558 
   559 goalw thy [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
   560 by (typ.induct_tac "t" 1);
   561 by (res_inst_tac [("x","Suc nat")] exI 1);
   562 by (Asm_simp_tac 1);
   563 by (REPEAT (etac exE 1));
   564 by (rename_tac "n'" 1);
   565 by (res_inst_tac [("x","max n n'")] exI 1);
   566 by (Simp_tac 1);
   567 by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1);
   568 qed "fresh_variable_types";
   569 
   570 Addsimps [fresh_variable_types];
   571 
   572 goalw thy [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)";
   573 by (type_scheme.induct_tac "sch" 1);
   574 by (res_inst_tac [("x","Suc nat")] exI 1);
   575 by (Simp_tac 1);
   576 by (res_inst_tac [("x","Suc nat")] exI 1);
   577 by (Simp_tac 1);
   578 by (REPEAT (etac exE 1));
   579 by (rename_tac "n'" 1);
   580 by (res_inst_tac [("x","max n n'")] exI 1);
   581 by (Simp_tac 1);
   582 by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1);
   583 qed "fresh_variable_type_schemes";
   584 
   585 Addsimps [fresh_variable_type_schemes];
   586 
   587 goalw thy [max_def] "!!n::nat. n <= (max n n')";
   588 by (simp_tac (simpset() addsplits [expand_if]) 1);
   589 val le_maxL = result();
   590 
   591 goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
   592 by (simp_tac (simpset() addsplits [expand_if]) 1);
   593 by (fast_tac (claset() addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
   594 val le_maxR = result();
   595 
   596 goal thy "!!A::type_scheme list. ? n. (new_tv n A)";
   597 by (list.induct_tac "A" 1);
   598 by (Simp_tac 1);
   599 by (Simp_tac 1);
   600 by (etac exE 1);
   601 by (cut_inst_tac [("sch","a")] fresh_variable_type_schemes 1);
   602 by (etac exE 1);
   603 by (rename_tac "n'" 1);
   604 by (res_inst_tac [("x","(max n n')")] exI 1);
   605 by (subgoal_tac "n <= (max n n')" 1);
   606 by (subgoal_tac "n' <= (max n n')" 1);
   607 by (fast_tac (claset() addDs [new_tv_le]) 1);
   608 by (ALLGOALS (simp_tac (simpset() addsimps [le_maxR,le_maxL])));
   609 qed "fresh_variable_type_scheme_lists";
   610 
   611 Addsimps [fresh_variable_type_scheme_lists];
   612 
   613 goal thy "!!x y. [| ? n1. (new_tv n1 x); ? n2. (new_tv n2 y)|] ==> ? n. (new_tv n x) & (new_tv n y)";
   614 by (REPEAT (etac exE 1));
   615 by (rename_tac "n1 n2" 1);
   616 by (res_inst_tac [("x","(max n1 n2)")] exI 1);
   617 by (subgoal_tac "n1 <= max n1 n2" 1);
   618 by (subgoal_tac "n2 <= max n1 n2" 1);
   619 by (fast_tac (claset() addDs [new_tv_le]) 1);
   620 by (ALLGOALS (simp_tac (simpset() addsimps [le_maxL,le_maxR])));
   621 qed "make_one_new_out_of_two";
   622 
   623 goal thy "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ). \
   624 \         ? n. (new_tv n A) & (new_tv n A') & (new_tv n t) & (new_tv n t')" ;
   625 by (cut_inst_tac [("t","t")] fresh_variable_types 1);
   626 by (cut_inst_tac [("t","t'")] fresh_variable_types 1);
   627 by (dtac make_one_new_out_of_two 1);
   628 by (assume_tac 1);
   629 by (thin_tac "? n. new_tv n t'" 1);
   630 by (cut_inst_tac [("A","A")] fresh_variable_type_scheme_lists 1);
   631 by (cut_inst_tac [("A","A'")] fresh_variable_type_scheme_lists 1);
   632 by (rotate_tac 1 1);
   633 by (dtac make_one_new_out_of_two 1);
   634 by (assume_tac 1);
   635 by (thin_tac "? n. new_tv n A'" 1);
   636 by (REPEAT (etac exE 1));
   637 by (rename_tac "n2 n1" 1);
   638 by (res_inst_tac [("x","(max n1 n2)")] exI 1);
   639 by (rewtac new_tv_def);
   640 by (fast_tac (claset() addIs [less_maxL,less_maxR]) 1);
   641 qed "ex_fresh_variable";
   642 
   643 (* mgu does not introduce new type variables *)
   644 goalw thy [new_tv_def] 
   645       "!! n. [|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> \
   646 \            new_tv n u";
   647 by (fast_tac (set_cs addDs [mgu_free]) 1);
   648 qed "mgu_new";
   649 
   650 
   651 (* lemmata for substitutions *)
   652 
   653 goalw Type.thy [app_subst_list] 
   654    "!!A:: ('a::type_struct) list. length ($ S A) = length A";
   655 by (Simp_tac 1);
   656 qed "length_app_subst_list";
   657 Addsimps [length_app_subst_list];
   658 
   659 goal thy "!!sch::type_scheme. $ TVar sch = sch";
   660 by (type_scheme.induct_tac "sch" 1);
   661 by (ALLGOALS Asm_simp_tac);
   662 qed "subst_TVar_scheme";
   663 
   664 Addsimps [subst_TVar_scheme];
   665 
   666 goal thy "!!A::type_scheme list. $ TVar A = A";
   667 by (rtac list.induct 1);
   668 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [app_subst_list])));
   669 qed "subst_TVar_scheme_list";
   670 
   671 Addsimps [subst_TVar_scheme_list];
   672 
   673 (* application of id_subst does not change type expression *)
   674 goalw thy [id_subst_def]
   675   "$ id_subst = (%t::typ. t)";
   676 by (rtac ext 1);
   677 by (typ.induct_tac "t" 1);
   678 by (ALLGOALS Asm_simp_tac);
   679 qed "app_subst_id_te";
   680 Addsimps [app_subst_id_te];
   681 
   682 goalw thy [id_subst_def]
   683   "$ id_subst = (%sch::type_scheme. sch)";
   684 by (rtac ext 1);
   685 by (type_scheme.induct_tac "t" 1);
   686 by (ALLGOALS Asm_simp_tac);
   687 qed "app_subst_id_type_scheme";
   688 Addsimps [app_subst_id_type_scheme];
   689 
   690 (* application of id_subst does not change list of type expressions *)
   691 goalw thy [app_subst_list]
   692   "$ id_subst = (%A::type_scheme list. A)";
   693 by (rtac ext 1); 
   694 by (list.induct_tac "A" 1);
   695 by (ALLGOALS Asm_simp_tac);
   696 qed "app_subst_id_tel";
   697 Addsimps [app_subst_id_tel];
   698 
   699 goal thy "!!sch::type_scheme. $ id_subst sch = sch";
   700 by (type_scheme.induct_tac "sch" 1);
   701 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [id_subst_def])));
   702 qed "id_subst_sch";
   703 
   704 Addsimps [id_subst_sch];
   705 
   706 goal thy "!!A::type_scheme list. $ id_subst A = A";
   707 by (list.induct_tac "A" 1);
   708 by (Asm_full_simp_tac 1);
   709 by (Asm_full_simp_tac 1);
   710 qed "id_subst_A";
   711 
   712 Addsimps [id_subst_A];
   713 
   714 (* composition of substitutions *)
   715 goalw Type.thy [id_subst_def,o_def] "$S o id_subst = S";
   716 by (rtac ext 1);
   717 by (Simp_tac 1);
   718 qed "o_id_subst";
   719 Addsimps[o_id_subst];
   720 
   721 goal thy
   722   "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t";
   723 by (typ.induct_tac "t" 1);
   724 by (ALLGOALS Asm_simp_tac);
   725 qed "subst_comp_te";
   726 
   727 goal thy
   728   "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch";
   729 by (type_scheme.induct_tac "sch" 1);
   730 by (ALLGOALS Asm_full_simp_tac);
   731 qed "subst_comp_type_scheme";
   732 
   733 goalw thy [app_subst_list]
   734   "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A";
   735 by (list.induct_tac "A" 1);
   736 (* case [] *)
   737 by (Simp_tac 1);
   738 (* case x#xl *)
   739 by (asm_full_simp_tac (simpset() addsimps [subst_comp_type_scheme]) 1);
   740 qed "subst_comp_scheme_list";
   741 
   742 goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = $ id_subst A";
   743 by (rtac scheme_list_substitutions_only_on_free_variables 1);
   744 by (asm_full_simp_tac (simpset() addsimps [id_subst_def]) 1);
   745 qed "subst_id_on_type_scheme_list'";
   746 
   747 goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A";
   748 by (stac subst_id_on_type_scheme_list' 1);
   749 by (assume_tac 1);
   750 by (Simp_tac 1);
   751 qed "subst_id_on_type_scheme_list";
   752 
   753 goal thy "!!n. !n. n < length A --> nth n ($ S A) = $S (nth n A)";
   754 by (list.induct_tac "A" 1);
   755 by (Asm_full_simp_tac 1);
   756 by (rtac allI 1);
   757 by (rename_tac "n1" 1);
   758 by (res_inst_tac[("n","n1")] nat_induct 1);
   759 by (Asm_full_simp_tac 1);
   760 by (Asm_full_simp_tac 1);
   761 qed_spec_mp "nth_subst";