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