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
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
wenzelm@3842
    19
goal thy "!t'. mk_scheme t = mk_scheme t' --> t=t'";
nipkow@2525
    20
by (typ.induct_tac "t" 1);
paulson@3018
    21
 by (rtac allI 1);
nipkow@2525
    22
 by (typ.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);
nipkow@2525
    26
by (typ.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@2525
    31
goal thy "!!t. free_tv (mk_scheme t) = free_tv t";
nipkow@2525
    32
by (typ.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@2525
    38
goal thy "!!t. $ S (mk_scheme t) = mk_scheme ($ S t)";
nipkow@1400
    39
by (typ.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
nipkow@2525
    48
goalw thy [app_subst_list]
nipkow@2525
    49
  "$ S [] = []";
nipkow@2525
    50
by (Simp_tac 1);
nipkow@2525
    51
qed "app_subst_Nil";
nipkow@2525
    52
nipkow@1300
    53
goalw thy [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
nipkow@2525
    63
goalw thy [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
nipkow@2525
    68
goalw thy [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
nipkow@2525
    73
goalw thy [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
nipkow@2525
    78
goalw thy [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
nipkow@2525
    83
goalw thy [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
nipkow@2525
    88
goalw thy [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
nipkow@2525
    93
goalw thy [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
narasche@2625
    98
goalw thy [new_tv_def] "!!n. 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
narasche@2625
   105
goalw thy [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
narasche@2625
   111
goal thy "new_tv n (sch::type_scheme) --> \
wenzelm@3842
   112
\              $(%k. if k<n then S k else S' k) sch = $S sch";
narasche@2625
   113
by (type_scheme.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
narasche@2625
   118
goal thy "new_tv n (A::type_scheme list) --> \
wenzelm@3842
   119
\              $(%k. if k<n then S k else S' k) A = $S A";
narasche@2625
   120
by (list.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
nipkow@1300
   128
goalw thy [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
nipkow@1300
   134
goalw thy [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
nipkow@1300
   143
goalw thy [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@2525
   149
goal thy "!!A. !n. n < length A --> x : free_tv (nth n A) --> x : free_tv A";
nipkow@2525
   150
by (list.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@2525
   160
goal thy "!!A. !nat. nat < length A --> x : free_tv (nth nat A) --> x : free_tv A";
nipkow@2525
   161
by (list.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@2525
   175
goal thy "!!S S'. (!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t";
nipkow@2525
   176
by (typ.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@2525
   181
goal thy
nipkow@2525
   182
  "!!t. (!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t";
nipkow@2525
   183
by (rtac typ_substitutions_only_on_free_variables 1);
wenzelm@4089
   184
by (simp_tac (simpset() addsimps [Ball_def]) 1);
nipkow@2525
   185
qed "eq_free_eq_subst_te";
nipkow@2525
   186
nipkow@2525
   187
goal thy "!!S S'. (!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch";
nipkow@2525
   188
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   189
by (Simp_tac 1);
nipkow@2525
   190
by (Simp_tac 1);
nipkow@2525
   191
by (Asm_full_simp_tac 1);
nipkow@2525
   192
qed_spec_mp "scheme_substitutions_only_on_free_variables";
nipkow@2525
   193
nipkow@2525
   194
goal thy
nipkow@2525
   195
  "!!sch. (!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch";
nipkow@2525
   196
by (rtac scheme_substitutions_only_on_free_variables 1);
wenzelm@4089
   197
by (simp_tac (simpset() addsimps [Ball_def]) 1);
nipkow@2525
   198
qed "eq_free_eq_subst_type_scheme";
nipkow@2525
   199
nipkow@2525
   200
goal thy
nipkow@2525
   201
  "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A";
nipkow@2525
   202
by (list.induct_tac "A" 1); 
nipkow@2525
   203
(* case [] *)
wenzelm@4089
   204
by (fast_tac (HOL_cs addss simpset()) 1);
nipkow@2525
   205
(* case x#xl *)
wenzelm@4089
   206
by (fast_tac (HOL_cs addIs [eq_free_eq_subst_type_scheme] addss (simpset())) 1);
nipkow@2525
   207
qed_spec_mp "eq_free_eq_subst_scheme_list";
nipkow@2525
   208
nipkow@2525
   209
goal thy "!!P Q. ((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)";
nipkow@2525
   210
by (Fast_tac 1);
nipkow@2525
   211
val weaken_asm_Un = result ();
nipkow@2525
   212
nipkow@2525
   213
goal thy "!!S S'. (!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A";
nipkow@2525
   214
by (list.induct_tac "A" 1);
nipkow@2525
   215
by (Simp_tac 1);
nipkow@2525
   216
by (Asm_full_simp_tac 1);
nipkow@2525
   217
by (rtac weaken_asm_Un 1);
nipkow@2525
   218
by (strip_tac 1);
nipkow@2525
   219
by (etac scheme_substitutions_only_on_free_variables 1);
nipkow@2525
   220
qed_spec_mp "scheme_list_substitutions_only_on_free_variables";
nipkow@2525
   221
nipkow@2525
   222
goal thy
nipkow@2525
   223
  "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n";
nipkow@2525
   224
by (typ.induct_tac "t" 1);
nipkow@2525
   225
(* case TVar n *)
wenzelm@4089
   226
by (fast_tac (HOL_cs addss simpset()) 1);
nipkow@2525
   227
(* case Fun t1 t2 *)
wenzelm@4089
   228
by (fast_tac (HOL_cs addss simpset()) 1);
nipkow@2525
   229
qed_spec_mp "eq_subst_te_eq_free";
nipkow@2525
   230
nipkow@2525
   231
goal thy
nipkow@2525
   232
  "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n";
nipkow@2525
   233
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   234
(* case TVar n *)
nipkow@2525
   235
by (Asm_simp_tac 1);
nipkow@2525
   236
(* case BVar n *)
nipkow@2525
   237
by (strip_tac 1);
nipkow@2525
   238
by (etac mk_scheme_injective 1);
nipkow@2525
   239
by (Asm_simp_tac 1);
nipkow@2525
   240
(* case Fun t1 t2 *)
nipkow@2525
   241
by (Asm_full_simp_tac 1);
nipkow@2525
   242
qed_spec_mp "eq_subst_type_scheme_eq_free";
nipkow@2525
   243
nipkow@2525
   244
goal thy
nipkow@2525
   245
  "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n";
nipkow@2525
   246
by (list.induct_tac "A" 1);
nipkow@2525
   247
(* case [] *)
wenzelm@4089
   248
by (fast_tac (HOL_cs addss simpset()) 1);
nipkow@2525
   249
(* case x#xl *)
wenzelm@4089
   250
by (fast_tac (HOL_cs addIs [eq_subst_type_scheme_eq_free] addss (simpset())) 1);
nipkow@2525
   251
qed_spec_mp "eq_subst_scheme_list_eq_free";
nipkow@2525
   252
nipkow@2525
   253
goalw thy [free_tv_subst] 
nipkow@2525
   254
      "!!v. v : cod S ==> v : free_tv S";
paulson@3385
   255
by (fast_tac set_cs 1);
nipkow@2525
   256
qed "codD";
nipkow@2525
   257
 
nipkow@2525
   258
goalw thy [free_tv_subst,dom_def] 
nipkow@2525
   259
      "!! x. x ~: free_tv S ==> S x = TVar x";
paulson@3385
   260
by (fast_tac set_cs 1);
nipkow@2525
   261
qed "not_free_impl_id";
nipkow@2525
   262
nipkow@2525
   263
goalw thy [new_tv_def] 
nipkow@2525
   264
      "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
paulson@3385
   265
by (fast_tac HOL_cs 1 );
nipkow@2525
   266
qed "free_tv_le_new_tv";
nipkow@2525
   267
nipkow@1300
   268
goalw thy [dom_def,cod_def,UNION_def,Bex_def]
nipkow@2525
   269
  "!!v. [| v : free_tv(S n); v~=n |] ==> v : cod S";
nipkow@1300
   270
by (Simp_tac 1);
nipkow@1300
   271
by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
clasohm@1465
   272
by (assume_tac 2);
nipkow@1300
   273
by (rotate_tac 1 1);
nipkow@1300
   274
by (Asm_full_simp_tac 1);
nipkow@1300
   275
qed "cod_app_subst";
nipkow@1300
   276
Addsimps [cod_app_subst];
nipkow@1300
   277
nipkow@1300
   278
goal thy 
paulson@3385
   279
     "free_tv (S (v::nat)) <= insert v (cod S)";
paulson@3385
   280
by (expand_case_tac "v:dom S" 1);
wenzelm@4089
   281
by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1);
wenzelm@4089
   282
by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1);
nipkow@1300
   283
qed "free_tv_subst_var";
nipkow@1300
   284
nipkow@1300
   285
goal thy 
nipkow@2525
   286
     "free_tv ($ S (t::typ)) <= cod S Un free_tv t";
paulson@3385
   287
by (typ.induct_tac "t" 1);
nipkow@1300
   288
(* case TVar n *)
wenzelm@4089
   289
by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
nipkow@1300
   290
(* case Fun t1 t2 *)
wenzelm@4089
   291
by (fast_tac (set_cs addss simpset()) 1);
nipkow@1300
   292
qed "free_tv_app_subst_te";     
nipkow@1300
   293
nipkow@1300
   294
goal thy 
nipkow@2525
   295
     "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
paulson@3385
   296
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   297
(* case FVar n *)
wenzelm@4089
   298
by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
nipkow@2525
   299
(* case BVar n *)
nipkow@2525
   300
by (Simp_tac 1);
nipkow@2525
   301
(* case Fun t1 t2 *)
wenzelm@4089
   302
by (fast_tac (set_cs addss simpset()) 1);
nipkow@2525
   303
qed "free_tv_app_subst_type_scheme";  
nipkow@2525
   304
nipkow@2525
   305
goal thy 
nipkow@2525
   306
     "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
paulson@3385
   307
by (list.induct_tac "A" 1);
nipkow@1300
   308
(* case [] *)
nipkow@1300
   309
by (Simp_tac 1);
nipkow@1300
   310
(* case a#al *)
paulson@3385
   311
by (cut_facts_tac [free_tv_app_subst_type_scheme] 1);
wenzelm@4089
   312
by (fast_tac (set_cs addss simpset()) 1);
nipkow@2525
   313
qed "free_tv_app_subst_scheme_list";
nipkow@1300
   314
nipkow@1521
   315
goalw thy [free_tv_subst,dom_def]
nipkow@1521
   316
     "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=   \
nipkow@1521
   317
\     free_tv s1 Un free_tv s2";
paulson@2513
   318
by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,
paulson@3008
   319
                             free_tv_subst_var RS subsetD] 
wenzelm@4089
   320
                     addss (simpset() delsimps bex_simps
paulson@3008
   321
                                     addsimps [cod_def,dom_def])) 1);
nipkow@1521
   322
qed "free_tv_comp_subst";
nipkow@1521
   323
nipkow@2525
   324
goalw thy [o_def] 
nipkow@2525
   325
     "free_tv ($ S1 o S2) <= free_tv S1 Un free_tv (S2 :: nat => typ)";
nipkow@2525
   326
by (rtac free_tv_comp_subst 1);
nipkow@2525
   327
qed "free_tv_o_subst";
nipkow@2525
   328
nipkow@2525
   329
goal thy "!!n. n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)";
nipkow@2525
   330
by (typ.induct_tac "t" 1);
nipkow@2525
   331
by (Simp_tac 1);
nipkow@2525
   332
by (Simp_tac 1);
nipkow@2525
   333
by (Fast_tac 1);
nipkow@2525
   334
qed_spec_mp "free_tv_of_substitutions_extend_to_types";
nipkow@2525
   335
nipkow@2525
   336
goal thy "!!n. n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)";
nipkow@2525
   337
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   338
by (Simp_tac 1);
nipkow@2525
   339
by (Simp_tac 1);
nipkow@2525
   340
by (Simp_tac 1);
nipkow@2525
   341
by (Fast_tac 1);
nipkow@2525
   342
qed_spec_mp "free_tv_of_substitutions_extend_to_schemes";
nipkow@2525
   343
nipkow@2525
   344
goal thy "!!n. n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)";
nipkow@2525
   345
by (list.induct_tac "A" 1);
nipkow@2525
   346
by (Simp_tac 1);
nipkow@2525
   347
by (Simp_tac 1);
wenzelm@4089
   348
by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_schemes]) 1);
nipkow@2525
   349
qed_spec_mp "free_tv_of_substitutions_extend_to_scheme_lists";
nipkow@2525
   350
nipkow@2525
   351
Addsimps [free_tv_of_substitutions_extend_to_scheme_lists];
nipkow@2525
   352
nipkow@2525
   353
goal thy "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
nipkow@2525
   354
by (type_scheme.induct_tac "sch" 1);
wenzelm@4089
   355
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
nipkow@2525
   356
by (strip_tac 1);
nipkow@2525
   357
by (Fast_tac 1);
nipkow@2525
   358
qed "free_tv_ML_scheme";
nipkow@2525
   359
nipkow@2525
   360
goal thy "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
nipkow@2525
   361
by (list.induct_tac "A" 1);
nipkow@2525
   362
by (Simp_tac 1);
wenzelm@4089
   363
by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme]) 1);
nipkow@2525
   364
qed "free_tv_ML_scheme_list";
nipkow@2525
   365
nipkow@2525
   366
nipkow@2525
   367
(* lemmata for bound_tv *)
nipkow@2525
   368
nipkow@2525
   369
goal thy "!!t. bound_tv (mk_scheme t) = {}";
nipkow@2525
   370
by (typ.induct_tac "t" 1);
nipkow@2525
   371
by (ALLGOALS Asm_simp_tac);
nipkow@2525
   372
qed "bound_tv_mk_scheme";
nipkow@2525
   373
nipkow@2525
   374
Addsimps [bound_tv_mk_scheme];
nipkow@2525
   375
nipkow@2525
   376
goal thy "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch";
nipkow@2525
   377
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   378
by (ALLGOALS Asm_simp_tac);
nipkow@2525
   379
qed "bound_tv_subst_scheme";
nipkow@2525
   380
nipkow@2525
   381
Addsimps [bound_tv_subst_scheme];
nipkow@2525
   382
nipkow@2525
   383
goal thy "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A";
nipkow@2525
   384
by (rtac list.induct 1);
nipkow@2525
   385
by (Simp_tac 1);
nipkow@2525
   386
by (Asm_simp_tac 1);
nipkow@2525
   387
qed "bound_tv_subst_scheme_list";
nipkow@2525
   388
nipkow@2525
   389
Addsimps [bound_tv_subst_scheme_list];
nipkow@2525
   390
nipkow@2525
   391
nipkow@2525
   392
(* lemmata for new_tv *)
nipkow@2525
   393
nipkow@2525
   394
goalw thy [new_tv_def]
nipkow@2525
   395
  "new_tv n S = ((!m. n <= m --> (S m = TVar m)) & \
nipkow@2525
   396
\                (! l. l < n --> new_tv n (S l) ))";
paulson@3385
   397
by (safe_tac HOL_cs );
nipkow@2525
   398
(* ==> *)
wenzelm@4089
   399
by (fast_tac (HOL_cs addDs [leD] addss (simpset() addsimps [free_tv_subst,dom_def])) 1);
paulson@3385
   400
by (subgoal_tac "m:cod S | S l = TVar l" 1);
paulson@3385
   401
by (safe_tac HOL_cs );
wenzelm@4089
   402
by (fast_tac (HOL_cs addDs [UnI2] addss (simpset() addsimps [free_tv_subst])) 1);
paulson@3018
   403
by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
paulson@3018
   404
by (Asm_full_simp_tac 1);
wenzelm@4089
   405
by (fast_tac (set_cs addss (simpset() addsimps [free_tv_subst,cod_def,dom_def])) 1);
nipkow@2525
   406
(* <== *)
paulson@3385
   407
by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
paulson@3385
   408
by (safe_tac set_cs );
paulson@3385
   409
by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
paulson@3385
   410
by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
paulson@3385
   411
by (cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
paulson@3385
   412
by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
nipkow@2525
   413
qed "new_tv_subst";
nipkow@2525
   414
nipkow@2525
   415
goal thy 
nipkow@2525
   416
  "new_tv n  = list_all (new_tv n)";
nipkow@2525
   417
by (rtac ext 1);
paulson@3018
   418
by (list.induct_tac "x" 1);
paulson@3018
   419
by (ALLGOALS Asm_simp_tac);
nipkow@2525
   420
qed "new_tv_list";
nipkow@2525
   421
nipkow@2525
   422
(* substitution affects only variables occurring freely *)
nipkow@2525
   423
goal thy
nipkow@2525
   424
  "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
nipkow@2525
   425
by (typ.induct_tac "t" 1);
wenzelm@4089
   426
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
nipkow@2525
   427
qed "subst_te_new_tv";
nipkow@2525
   428
Addsimps [subst_te_new_tv];
nipkow@2525
   429
nipkow@2525
   430
goal thy
nipkow@2525
   431
  "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
nipkow@2525
   432
by (type_scheme.induct_tac "sch" 1);
wenzelm@4089
   433
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
nipkow@2525
   434
qed_spec_mp "subst_te_new_type_scheme";
nipkow@2525
   435
Addsimps [subst_te_new_type_scheme];
nipkow@2525
   436
nipkow@2525
   437
goal thy
nipkow@2525
   438
  "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A";
nipkow@2525
   439
by (list.induct_tac "A" 1);
nipkow@2525
   440
by (ALLGOALS Asm_full_simp_tac);
nipkow@2525
   441
qed_spec_mp "subst_tel_new_scheme_list";
nipkow@2525
   442
Addsimps [subst_tel_new_scheme_list];
nipkow@2525
   443
nipkow@2525
   444
(* all greater variables are also new *)
nipkow@2525
   445
goalw thy [new_tv_def] 
nipkow@2525
   446
  "!!n m. n<=m ==> new_tv n t ==> new_tv m t";
paulson@4153
   447
by Safe_tac;
nipkow@2525
   448
by (dtac spec 1);
nipkow@2525
   449
by (mp_tac 1);
nipkow@2525
   450
by (trans_tac 1);
nipkow@2525
   451
qed "new_tv_le";
nipkow@2525
   452
Addsimps [lessI RS less_imp_le RS new_tv_le];
nipkow@2525
   453
nipkow@2525
   454
goal thy "!!n m. n<=m ==> new_tv n (t::typ) ==> new_tv m t";
wenzelm@4089
   455
by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
nipkow@2525
   456
qed "new_tv_typ_le";
nipkow@2525
   457
nipkow@2525
   458
goal thy "!!n m. n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A";
wenzelm@4089
   459
by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
nipkow@2525
   460
qed "new_scheme_list_le";
nipkow@2525
   461
nipkow@2525
   462
goal thy "!!n m. n<=m ==> new_tv n (S::subst) ==> new_tv m S";
wenzelm@4089
   463
by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
nipkow@2525
   464
qed "new_tv_subst_le";
nipkow@2525
   465
nipkow@2525
   466
(* new_tv property remains if a substitution is applied *)
nipkow@2525
   467
goal thy
nipkow@2525
   468
  "!!n. [| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)";
wenzelm@4089
   469
by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
nipkow@2525
   470
qed "new_tv_subst_var";
nipkow@2525
   471
nipkow@2525
   472
goal thy
nipkow@2525
   473
  "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)";
nipkow@2525
   474
by (typ.induct_tac "t" 1);
wenzelm@4089
   475
by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
nipkow@2525
   476
qed_spec_mp "new_tv_subst_te";
nipkow@2525
   477
Addsimps [new_tv_subst_te];
nipkow@2525
   478
nipkow@2525
   479
goal thy "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)";
nipkow@2525
   480
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   481
by (ALLGOALS (Asm_full_simp_tac));
paulson@3008
   482
by (rewtac new_tv_def);
wenzelm@4089
   483
by (simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1);
nipkow@2525
   484
by (strip_tac 1);
nipkow@2525
   485
by (case_tac "S nat = TVar nat" 1);
nipkow@2525
   486
by (rotate_tac 3 1);
nipkow@2525
   487
by (Asm_full_simp_tac 1);
nipkow@2525
   488
by (dres_inst_tac [("x","m")] spec 1);
nipkow@2525
   489
by (Fast_tac 1);
nipkow@2525
   490
qed_spec_mp "new_tv_subst_type_scheme";
nipkow@2525
   491
Addsimps [new_tv_subst_type_scheme];
nipkow@2525
   492
nipkow@2525
   493
goal thy
nipkow@2525
   494
  "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)";
nipkow@2525
   495
by (list.induct_tac "A" 1);
wenzelm@4089
   496
by (ALLGOALS(fast_tac (HOL_cs addss (simpset()))));
nipkow@2525
   497
qed_spec_mp "new_tv_subst_scheme_list";
nipkow@2525
   498
Addsimps [new_tv_subst_scheme_list];
nipkow@2525
   499
nipkow@2525
   500
goal thy
nipkow@2525
   501
  "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
wenzelm@4089
   502
by (simp_tac (simpset() addsimps [new_tv_list]) 1);
nipkow@2525
   503
by (list.induct_tac "A" 1);
nipkow@2525
   504
by (ALLGOALS Asm_full_simp_tac);
nipkow@2525
   505
qed "new_tv_Suc_list";
nipkow@2525
   506
nipkow@2525
   507
goalw thy [new_tv_def] "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')";
nipkow@2525
   508
by (Asm_simp_tac 1);
nipkow@2525
   509
qed_spec_mp "new_tv_only_depends_on_free_tv_type_scheme";
nipkow@2525
   510
nipkow@2525
   511
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
   512
by (Asm_simp_tac 1);
nipkow@2525
   513
qed_spec_mp "new_tv_only_depends_on_free_tv_scheme_list";
nipkow@2525
   514
nipkow@2525
   515
goalw thy [new_tv_def] "!!A. !nat. nat < length A --> new_tv n A --> (new_tv n (nth nat A))";
nipkow@2525
   516
by (list.induct_tac "A" 1);
nipkow@2525
   517
by (Asm_full_simp_tac 1);
nipkow@2525
   518
by (rtac allI 1);
nipkow@2525
   519
by (res_inst_tac [("n","nat")] nat_induct 1);
nipkow@2525
   520
by (strip_tac 1);
nipkow@2525
   521
by (Asm_full_simp_tac 1);
nipkow@2525
   522
by (Simp_tac 1);
nipkow@2525
   523
qed_spec_mp "new_tv_nth_nat_A";
nipkow@2525
   524
nipkow@2525
   525
nipkow@2525
   526
(* composition of substitutions preserves new_tv proposition *)
nipkow@2525
   527
goal thy 
nipkow@2525
   528
     "!! n. [| new_tv n (S::subst); new_tv n R |] ==> \
nipkow@2525
   529
\           new_tv n (($ R) o S)";
wenzelm@4089
   530
by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
nipkow@2525
   531
qed "new_tv_subst_comp_1";
nipkow@2525
   532
nipkow@2525
   533
goal thy
nipkow@2525
   534
     "!! n. [| new_tv n (S::subst); new_tv n R |] ==>  \ 
nipkow@2525
   535
\     new_tv n (%v.$ R (S v))";
wenzelm@4089
   536
by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
nipkow@2525
   537
qed "new_tv_subst_comp_2";
nipkow@2525
   538
nipkow@2525
   539
Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2];
nipkow@2525
   540
nipkow@2525
   541
(* new type variables do not occur freely in a type structure *)
nipkow@2525
   542
goalw thy [new_tv_def] 
nipkow@2525
   543
      "!!n. new_tv n A ==> n~:(free_tv A)";
nipkow@2525
   544
by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
nipkow@2525
   545
qed "new_tv_not_free_tv";
nipkow@2525
   546
Addsimps [new_tv_not_free_tv];
nipkow@2525
   547
nipkow@2525
   548
goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
wenzelm@4089
   549
by (simp_tac (simpset() addsplits [expand_if]) 1);
paulson@4153
   550
by Safe_tac;
nipkow@2525
   551
by (trans_tac 1);
nipkow@2525
   552
qed "less_maxL";
nipkow@2525
   553
nipkow@2525
   554
goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
wenzelm@4089
   555
by (simp_tac (simpset() addsplits [expand_if]) 1);
wenzelm@4089
   556
by (fast_tac (claset() addDs [not_leE] addIs [less_trans]) 1);
narasche@2625
   557
val less_maxR = result();
nipkow@2525
   558
nipkow@2525
   559
goalw thy [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
nipkow@2525
   560
by (typ.induct_tac "t" 1);
nipkow@2525
   561
by (res_inst_tac [("x","Suc nat")] exI 1);
nipkow@2525
   562
by (Asm_simp_tac 1);
nipkow@2525
   563
by (REPEAT (etac exE 1));
nipkow@2525
   564
by (rename_tac "n'" 1);
nipkow@2525
   565
by (res_inst_tac [("x","max n n'")] exI 1);
nipkow@2525
   566
by (Simp_tac 1);
wenzelm@4089
   567
by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1);
nipkow@2525
   568
qed "fresh_variable_types";
nipkow@2525
   569
nipkow@2525
   570
Addsimps [fresh_variable_types];
nipkow@2525
   571
nipkow@2525
   572
goalw thy [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)";
nipkow@2525
   573
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   574
by (res_inst_tac [("x","Suc nat")] exI 1);
nipkow@2525
   575
by (Simp_tac 1);
nipkow@2525
   576
by (res_inst_tac [("x","Suc nat")] exI 1);
nipkow@2525
   577
by (Simp_tac 1);
nipkow@2525
   578
by (REPEAT (etac exE 1));
nipkow@2525
   579
by (rename_tac "n'" 1);
nipkow@2525
   580
by (res_inst_tac [("x","max n n'")] exI 1);
nipkow@2525
   581
by (Simp_tac 1);
wenzelm@4089
   582
by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1);
nipkow@2525
   583
qed "fresh_variable_type_schemes";
nipkow@2525
   584
nipkow@2525
   585
Addsimps [fresh_variable_type_schemes];
nipkow@2525
   586
nipkow@2525
   587
goalw thy [max_def] "!!n::nat. n <= (max n n')";
wenzelm@4089
   588
by (simp_tac (simpset() addsplits [expand_if]) 1);
narasche@2625
   589
val le_maxL = result();
nipkow@2525
   590
nipkow@2525
   591
goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
wenzelm@4089
   592
by (simp_tac (simpset() addsplits [expand_if]) 1);
wenzelm@4089
   593
by (fast_tac (claset() addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
narasche@2625
   594
val le_maxR = result();
nipkow@2525
   595
nipkow@2525
   596
goal thy "!!A::type_scheme list. ? n. (new_tv n A)";
nipkow@2525
   597
by (list.induct_tac "A" 1);
nipkow@2525
   598
by (Simp_tac 1);
nipkow@2525
   599
by (Simp_tac 1);
nipkow@2525
   600
by (etac exE 1);
nipkow@2525
   601
by (cut_inst_tac [("sch","a")] fresh_variable_type_schemes 1);
nipkow@2525
   602
by (etac exE 1);
nipkow@2525
   603
by (rename_tac "n'" 1);
nipkow@2525
   604
by (res_inst_tac [("x","(max n n')")] exI 1);
nipkow@2525
   605
by (subgoal_tac "n <= (max n n')" 1);
nipkow@2525
   606
by (subgoal_tac "n' <= (max n n')" 1);
wenzelm@4089
   607
by (fast_tac (claset() addDs [new_tv_le]) 1);
wenzelm@4089
   608
by (ALLGOALS (simp_tac (simpset() addsimps [le_maxR,le_maxL])));
nipkow@2525
   609
qed "fresh_variable_type_scheme_lists";
nipkow@2525
   610
nipkow@2525
   611
Addsimps [fresh_variable_type_scheme_lists];
nipkow@2525
   612
nipkow@2525
   613
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
   614
by (REPEAT (etac exE 1));
nipkow@2525
   615
by (rename_tac "n1 n2" 1);
nipkow@2525
   616
by (res_inst_tac [("x","(max n1 n2)")] exI 1);
nipkow@2525
   617
by (subgoal_tac "n1 <= max n1 n2" 1);
nipkow@2525
   618
by (subgoal_tac "n2 <= max n1 n2" 1);
wenzelm@4089
   619
by (fast_tac (claset() addDs [new_tv_le]) 1);
wenzelm@4089
   620
by (ALLGOALS (simp_tac (simpset() addsimps [le_maxL,le_maxR])));
nipkow@2525
   621
qed "make_one_new_out_of_two";
nipkow@2525
   622
nipkow@2525
   623
goal thy "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ). \
nipkow@2525
   624
\         ? n. (new_tv n A) & (new_tv n A') & (new_tv n t) & (new_tv n t')" ;
nipkow@2525
   625
by (cut_inst_tac [("t","t")] fresh_variable_types 1);
nipkow@2525
   626
by (cut_inst_tac [("t","t'")] fresh_variable_types 1);
nipkow@2525
   627
by (dtac make_one_new_out_of_two 1);
paulson@3018
   628
by (assume_tac 1);
nipkow@2525
   629
by (thin_tac "? n. new_tv n t'" 1);
nipkow@2525
   630
by (cut_inst_tac [("A","A")] fresh_variable_type_scheme_lists 1);
nipkow@2525
   631
by (cut_inst_tac [("A","A'")] fresh_variable_type_scheme_lists 1);
nipkow@2525
   632
by (rotate_tac 1 1);
nipkow@2525
   633
by (dtac make_one_new_out_of_two 1);
paulson@3018
   634
by (assume_tac 1);
nipkow@2525
   635
by (thin_tac "? n. new_tv n A'" 1);
nipkow@2525
   636
by (REPEAT (etac exE 1));
nipkow@2525
   637
by (rename_tac "n2 n1" 1);
nipkow@2525
   638
by (res_inst_tac [("x","(max n1 n2)")] exI 1);
paulson@3008
   639
by (rewtac new_tv_def);
wenzelm@4089
   640
by (fast_tac (claset() addIs [less_maxL,less_maxR]) 1);
nipkow@2525
   641
qed "ex_fresh_variable";
nipkow@2525
   642
nipkow@2525
   643
(* mgu does not introduce new type variables *)
nipkow@2525
   644
goalw thy [new_tv_def] 
nipkow@2525
   645
      "!! n. [|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> \
nipkow@2525
   646
\            new_tv n u";
paulson@3385
   647
by (fast_tac (set_cs addDs [mgu_free]) 1);
nipkow@2525
   648
qed "mgu_new";
nipkow@2525
   649
nipkow@2525
   650
nipkow@2525
   651
(* lemmata for substitutions *)
nipkow@2525
   652
paulson@3438
   653
goalw Type.thy [app_subst_list] 
paulson@3438
   654
   "!!A:: ('a::type_struct) list. length ($ S A) = length A";
paulson@3018
   655
by (Simp_tac 1);
nipkow@2525
   656
qed "length_app_subst_list";
nipkow@2525
   657
Addsimps [length_app_subst_list];
nipkow@2525
   658
nipkow@2525
   659
goal thy "!!sch::type_scheme. $ TVar sch = sch";
nipkow@2525
   660
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   661
by (ALLGOALS Asm_simp_tac);
nipkow@2525
   662
qed "subst_TVar_scheme";
nipkow@2525
   663
nipkow@2525
   664
Addsimps [subst_TVar_scheme];
nipkow@2525
   665
nipkow@2525
   666
goal thy "!!A::type_scheme list. $ TVar A = A";
nipkow@2525
   667
by (rtac list.induct 1);
wenzelm@4089
   668
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [app_subst_list])));
nipkow@2525
   669
qed "subst_TVar_scheme_list";
nipkow@2525
   670
nipkow@2525
   671
Addsimps [subst_TVar_scheme_list];
nipkow@2525
   672
nipkow@2525
   673
(* application of id_subst does not change type expression *)
nipkow@2525
   674
goalw thy [id_subst_def]
wenzelm@3842
   675
  "$ id_subst = (%t::typ. t)";
nipkow@2525
   676
by (rtac ext 1);
nipkow@2525
   677
by (typ.induct_tac "t" 1);
nipkow@2525
   678
by (ALLGOALS Asm_simp_tac);
nipkow@2525
   679
qed "app_subst_id_te";
nipkow@2525
   680
Addsimps [app_subst_id_te];
nipkow@2525
   681
nipkow@2525
   682
goalw thy [id_subst_def]
wenzelm@3842
   683
  "$ id_subst = (%sch::type_scheme. sch)";
nipkow@2525
   684
by (rtac ext 1);
nipkow@2525
   685
by (type_scheme.induct_tac "t" 1);
nipkow@2525
   686
by (ALLGOALS Asm_simp_tac);
nipkow@2525
   687
qed "app_subst_id_type_scheme";
nipkow@2525
   688
Addsimps [app_subst_id_type_scheme];
nipkow@2525
   689
nipkow@2525
   690
(* application of id_subst does not change list of type expressions *)
nipkow@2525
   691
goalw thy [app_subst_list]
wenzelm@3842
   692
  "$ id_subst = (%A::type_scheme list. A)";
nipkow@2525
   693
by (rtac ext 1); 
nipkow@2525
   694
by (list.induct_tac "A" 1);
nipkow@2525
   695
by (ALLGOALS Asm_simp_tac);
nipkow@2525
   696
qed "app_subst_id_tel";
nipkow@2525
   697
Addsimps [app_subst_id_tel];
nipkow@2525
   698
nipkow@2525
   699
goal thy "!!sch::type_scheme. $ id_subst sch = sch";
nipkow@2525
   700
by (type_scheme.induct_tac "sch" 1);
wenzelm@4089
   701
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [id_subst_def])));
nipkow@2525
   702
qed "id_subst_sch";
nipkow@2525
   703
nipkow@2525
   704
Addsimps [id_subst_sch];
nipkow@2525
   705
nipkow@2525
   706
goal thy "!!A::type_scheme list. $ id_subst A = A";
nipkow@2525
   707
by (list.induct_tac "A" 1);
nipkow@2525
   708
by (Asm_full_simp_tac 1);
nipkow@2525
   709
by (Asm_full_simp_tac 1);
nipkow@2525
   710
qed "id_subst_A";
nipkow@2525
   711
nipkow@2525
   712
Addsimps [id_subst_A];
nipkow@2525
   713
nipkow@2525
   714
(* composition of substitutions *)
nipkow@2525
   715
goalw Type.thy [id_subst_def,o_def] "$S o id_subst = S";
paulson@3018
   716
by (rtac ext 1);
paulson@3018
   717
by (Simp_tac 1);
nipkow@2525
   718
qed "o_id_subst";
nipkow@2525
   719
Addsimps[o_id_subst];
nipkow@2525
   720
nipkow@2525
   721
goal thy
nipkow@2525
   722
  "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t";
nipkow@2525
   723
by (typ.induct_tac "t" 1);
nipkow@2525
   724
by (ALLGOALS Asm_simp_tac);
nipkow@2525
   725
qed "subst_comp_te";
nipkow@2525
   726
nipkow@2525
   727
goal thy
nipkow@2525
   728
  "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch";
nipkow@2525
   729
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   730
by (ALLGOALS Asm_full_simp_tac);
nipkow@2525
   731
qed "subst_comp_type_scheme";
nipkow@2525
   732
nipkow@2525
   733
goalw thy [app_subst_list]
nipkow@2525
   734
  "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A";
nipkow@2525
   735
by (list.induct_tac "A" 1);
nipkow@2525
   736
(* case [] *)
nipkow@2525
   737
by (Simp_tac 1);
nipkow@2525
   738
(* case x#xl *)
wenzelm@4089
   739
by (asm_full_simp_tac (simpset() addsimps [subst_comp_type_scheme]) 1);
nipkow@2525
   740
qed "subst_comp_scheme_list";
nipkow@2525
   741
nipkow@2525
   742
goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = $ id_subst A";
nipkow@2525
   743
by (rtac scheme_list_substitutions_only_on_free_variables 1);
wenzelm@4089
   744
by (asm_full_simp_tac (simpset() addsimps [id_subst_def]) 1);
nipkow@2525
   745
qed "subst_id_on_type_scheme_list'";
nipkow@2525
   746
nipkow@2525
   747
goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A";
nipkow@2525
   748
by (stac subst_id_on_type_scheme_list' 1);
paulson@3018
   749
by (assume_tac 1);
nipkow@2525
   750
by (Simp_tac 1);
nipkow@2525
   751
qed "subst_id_on_type_scheme_list";
nipkow@2525
   752
nipkow@2525
   753
goal thy "!!n. !n. n < length A --> nth n ($ S A) = $S (nth n A)";
nipkow@2525
   754
by (list.induct_tac "A" 1);
nipkow@2525
   755
by (Asm_full_simp_tac 1);
nipkow@2525
   756
by (rtac allI 1);
nipkow@2525
   757
by (rename_tac "n1" 1);
nipkow@2525
   758
by (res_inst_tac[("n","n1")] nat_induct 1);
nipkow@2525
   759
by (Asm_full_simp_tac 1);
nipkow@2525
   760
by (Asm_full_simp_tac 1);
nipkow@2525
   761
qed_spec_mp "nth_subst";