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