src/HOL/MiniML/W.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@1300
     1
(* Title:     HOL/MiniML/W.ML
nipkow@1300
     2
   ID:        $Id$
nipkow@1300
     3
   Author:    Dieter Nazareth and Tobias Nipkow
nipkow@1300
     4
   Copyright  1995 TU Muenchen
nipkow@1300
     5
nipkow@1300
     6
Correctness and completeness of type inference algorithm W
nipkow@1300
     7
*)
nipkow@1300
     8
nipkow@1300
     9
open W;
nipkow@1300
    10
nipkow@2525
    11
Addsimps [diff_add_inverse,diff_add_inverse2,Suc_le_lessD];
nipkow@1300
    12
nipkow@1300
    13
val has_type_casesE = map(has_type.mk_cases expr.simps)
nipkow@2525
    14
        [" A |- Var n :: t"," A |- Abs e :: t","A |- App e1 e2 ::t","A |- LET e1 e2 ::t" ];
nipkow@1300
    15
nipkow@1300
    16
(* the resulting type variable is always greater or equal than the given one *)
nipkow@1300
    17
goal thy
nipkow@2525
    18
        "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
nipkow@1300
    19
by (expr.induct_tac "e" 1);
nipkow@1300
    20
(* case Var(n) *)
nipkow@2525
    21
by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
nipkow@2525
    22
by (strip_tac 1);
nipkow@2525
    23
by (etac conjE 1);
nipkow@2525
    24
by (etac conjE 1);
nipkow@2525
    25
by (dtac sym 1);
nipkow@2525
    26
by (dtac sym 1);
nipkow@2525
    27
by (dtac sym 1);
nipkow@2525
    28
by (Asm_full_simp_tac 1);
nipkow@1300
    29
(* case Abs e *)
nipkow@2525
    30
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
nipkow@1300
    31
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
nipkow@1300
    32
(* case App e1 e2 *)
nipkow@2525
    33
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
nipkow@1300
    34
by (strip_tac 1);
nipkow@2525
    35
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
nipkow@2525
    36
by (eres_inst_tac [("x","A")] allE 1);
nipkow@1300
    37
by (eres_inst_tac [("x","n")] allE 1);
nipkow@2525
    38
by (eres_inst_tac [("x","$ S A")] allE 1);
nipkow@2525
    39
by (eres_inst_tac [("x","S")] allE 1);
nipkow@1300
    40
by (eres_inst_tac [("x","t")] allE 1);
nipkow@2525
    41
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@2525
    42
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@1300
    43
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
nipkow@1300
    44
by (etac conjE 1);
nipkow@2525
    45
by (eres_inst_tac [("x","S1")] allE 1);
nipkow@2525
    46
by (eres_inst_tac [("x","t1")] allE 1);
nipkow@2525
    47
by (eres_inst_tac [("x","n2")] allE 1);
nipkow@1300
    48
by (etac conjE 1);
nipkow@2525
    49
by (res_inst_tac [("j","n1")] le_trans 1); 
nipkow@1300
    50
by (Asm_simp_tac 1);
nipkow@1669
    51
by (Asm_simp_tac 1);
nipkow@2525
    52
(* case LET e1 e2 *)
nipkow@2525
    53
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
nipkow@2525
    54
by (strip_tac 1);
nipkow@2525
    55
by (rename_tac "A n1 S t2 m1 S2 t3 m2 S3 t1 m" 1);
nipkow@2525
    56
by (REPEAT (etac conjE 1));
nipkow@2525
    57
by (REPEAT (etac allE 1));
nipkow@2525
    58
by (mp_tac 1);
nipkow@2525
    59
by (mp_tac 1);
nipkow@2525
    60
by (best_tac (!claset addEs [le_trans]) 1);
nipkow@1486
    61
qed_spec_mp "W_var_ge";
nipkow@1300
    62
nipkow@1300
    63
Addsimps [W_var_ge];
nipkow@1300
    64
nipkow@1300
    65
goal thy
nipkow@2525
    66
        "!! s. Some (S,t,m) = W e A n ==> n<=m";
nipkow@1300
    67
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
nipkow@1300
    68
qed "W_var_geD";
nipkow@1300
    69
nipkow@2525
    70
goal thy "!! s. new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A";
nipkow@2525
    71
by (dtac W_var_geD 1);
nipkow@2525
    72
by (rtac new_scheme_list_le 1);
nipkow@2525
    73
ba 1;
nipkow@2525
    74
ba 1;
nipkow@2525
    75
qed "new_tv_compatible_W";
nipkow@1300
    76
nipkow@1300
    77
(* auxiliary lemma *)
nipkow@2525
    78
goal Maybe.thy "(y = Some x) = (Some x = y)";
nipkow@2525
    79
by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
nipkow@2525
    80
qed "rotate_Some";
nipkow@1300
    81
nipkow@2525
    82
goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
nipkow@2525
    83
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
    84
by (Asm_full_simp_tac 1);
nipkow@2525
    85
by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
nipkow@2525
    86
by (strip_tac 1);
nipkow@2525
    87
by (Asm_full_simp_tac 1);
nipkow@2525
    88
by (etac conjE 1);
nipkow@2525
    89
by (rtac conjI 1);
nipkow@2525
    90
by (rtac new_tv_le 1);
nipkow@2525
    91
by (mp_tac 2);
nipkow@2525
    92
by (mp_tac 2);
nipkow@2525
    93
ba 2;
nipkow@2525
    94
by (rtac add_le_mono 1);
nipkow@2525
    95
by (Simp_tac 1);
nipkow@2525
    96
by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
nipkow@2525
    97
by (strip_tac 1);
nipkow@2525
    98
by (rtac new_tv_le 1);
nipkow@2525
    99
by (mp_tac 2);
nipkow@2525
   100
by (mp_tac 2);
nipkow@2525
   101
ba 2;
nipkow@2525
   102
by (rtac add_le_mono 1);
nipkow@2525
   103
by (Simp_tac 1);
nipkow@2525
   104
by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
nipkow@2525
   105
by (strip_tac 1);
nipkow@2525
   106
by (dtac not_leE 1);
nipkow@2525
   107
by (rtac less_or_eq_imp_le 1);
nipkow@2525
   108
by (Fast_tac 1);
nipkow@2525
   109
qed_spec_mp "new_tv_bound_typ_inst_sch";
nipkow@2525
   110
nipkow@2525
   111
Addsimps [new_tv_bound_typ_inst_sch];
nipkow@1300
   112
nipkow@1300
   113
(* resulting type variable is new *)
nipkow@1300
   114
goal thy
nipkow@2525
   115
     "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
nipkow@2525
   116
\                 new_tv m S & new_tv m t";
nipkow@1300
   117
by (expr.induct_tac "e" 1);
nipkow@1300
   118
(* case Var n *)
nipkow@2525
   119
by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
nipkow@2525
   120
by (strip_tac 1);
nipkow@2525
   121
by (REPEAT (etac conjE 1));
nipkow@2525
   122
by (rtac conjI 1);
nipkow@2525
   123
by (dtac sym 1);
nipkow@2525
   124
by (Asm_full_simp_tac 1);
nipkow@2525
   125
by (dtac sym 1);
nipkow@2525
   126
by (dtac sym 1);
nipkow@2525
   127
by (dtac sym 1);
nipkow@2525
   128
by (dtac new_tv_nth_nat_A 1);
nipkow@2525
   129
ba 1;
nipkow@2525
   130
by (Asm_full_simp_tac 1);
nipkow@1300
   131
(* case Abs e *)
nipkow@1300
   132
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
nipkow@2525
   133
    setloop (split_tac [expand_option_bind])) 1);
nipkow@1300
   134
by (strip_tac 1);
nipkow@1300
   135
by (eres_inst_tac [("x","Suc n")] allE 1);
nipkow@2525
   136
by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
nipkow@1300
   137
by (fast_tac (HOL_cs addss (!simpset
clasohm@1465
   138
              addsimps [new_tv_subst,new_tv_Suc_list])) 1);
nipkow@1300
   139
(* case App e1 e2 *)
nipkow@2525
   140
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
nipkow@1300
   141
by (strip_tac 1);
nipkow@2525
   142
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
nipkow@1300
   143
by (eres_inst_tac [("x","n")] allE 1);
nipkow@2525
   144
by (eres_inst_tac [("x","A")] allE 1);
nipkow@2525
   145
by (eres_inst_tac [("x","S")] allE 1);
nipkow@1300
   146
by (eres_inst_tac [("x","t")] allE 1);
nipkow@2525
   147
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@2525
   148
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@2525
   149
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv] delsimps all_simps) 1);
nipkow@2525
   150
by (eres_inst_tac [("x","$ S A")] allE 1);
nipkow@2525
   151
by (eres_inst_tac [("x","S1")] allE 1);
nipkow@2525
   152
by (eres_inst_tac [("x","t1")] allE 1);
nipkow@2525
   153
by (eres_inst_tac [("x","n2")] allE 1);
nipkow@2525
   154
by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 1);
nipkow@1300
   155
by (rtac conjI 1);
nipkow@1300
   156
by (rtac new_tv_subst_comp_2 1);
nipkow@1300
   157
by (rtac new_tv_subst_comp_2 1);
nipkow@2525
   158
by (rtac (lessI RS less_imp_le RS new_tv_le) 1); 
nipkow@2525
   159
by (res_inst_tac [("n","n1")] new_tv_subst_le 1); 
nipkow@2525
   160
by (asm_full_simp_tac (!simpset addsimps [rotate_Some]) 1);
nipkow@1300
   161
by (Asm_simp_tac 1);
nipkow@1300
   162
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
nipkow@2525
   163
     [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_subst_le])
nipkow@1300
   164
    1);
clasohm@1465
   165
by (etac (sym RS mgu_new) 1);
nipkow@2525
   166
by (best_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_scheme_list_le,
nipkow@2525
   167
   new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS 
nipkow@2525
   168
   new_tv_subst_le,new_tv_le]) 1);
nipkow@2525
   169
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
nipkow@2525
   170
     [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] 
nipkow@2525
   171
        addss (!simpset)) 1);
clasohm@1465
   172
by (rtac (lessI RS new_tv_subst_var) 1);
clasohm@1465
   173
by (etac (sym RS mgu_new) 1);
paulson@1925
   174
by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
nipkow@2525
   175
   addDs [W_var_geD] addIs
nipkow@2525
   176
   [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS
nipkow@2525
   177
   new_tv_subst_le,new_tv_le] addss !simpset) 1);
nipkow@2525
   178
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
nipkow@2525
   179
     [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
nipkow@2525
   180
     addss (!simpset)) 1);
nipkow@2525
   181
(* case LET e1 e2 *)
nipkow@2525
   182
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
nipkow@2525
   183
by (strip_tac 1);
nipkow@2525
   184
by (rename_tac "n1 A S1 t1 n2 S2 t2 m2 S t m" 1);
nipkow@2525
   185
by (REPEAT (etac conjE 1));
nipkow@2525
   186
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@2525
   187
by (eres_inst_tac [("x","A")] allE 1);
nipkow@2525
   188
by (eres_inst_tac [("x","S1")] allE 1);
nipkow@2525
   189
by (eres_inst_tac [("x","t1")] allE 1);
nipkow@2525
   190
by (rotate_tac 1 1);
nipkow@2525
   191
by (eres_inst_tac [("x","n2")] allE 1);
nipkow@2525
   192
by (mp_tac 1);
nipkow@2525
   193
by (mp_tac 1);
nipkow@2525
   194
by (etac conjE 1);
nipkow@2525
   195
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv] delsimps all_simps) 1);
nipkow@2525
   196
by (dtac sym 1);
nipkow@2525
   197
by (eres_inst_tac [("x","n2")] allE 1);
nipkow@2525
   198
by (eres_inst_tac [("x","gen ($ S1 A) t1 # $ S1 A")] allE 1);
nipkow@2525
   199
by (eres_inst_tac [("x","S2")] allE 1);
nipkow@2525
   200
by (eres_inst_tac [("x","t2")] allE 1);
nipkow@2525
   201
by (eres_inst_tac [("x","m2")] allE 1);
nipkow@2525
   202
by (subgoal_tac "new_tv n2 (gen ($ S1 A) t1 # $ S1 A)" 1);
nipkow@2525
   203
by (mp_tac 1);
nipkow@2525
   204
by (mp_tac 1);
nipkow@2525
   205
by (etac conjE 1);
nipkow@2525
   206
by (rtac conjI 1);
nipkow@2525
   207
by (simp_tac (!simpset addsimps [o_def]) 1);
nipkow@2525
   208
by (rtac new_tv_subst_comp_2 1);
nipkow@2525
   209
by (res_inst_tac [("n","n2")] new_tv_subst_le 1);
nipkow@2525
   210
by (etac W_var_ge 1);
nipkow@2525
   211
ba 1;
nipkow@2525
   212
ba 1;
nipkow@2525
   213
ba 1;
nipkow@2525
   214
by (rewrite_goals_tac [new_tv_def]);
nipkow@2525
   215
by (Asm_simp_tac 1);
nipkow@2525
   216
by (dtac W_var_ge 1);
nipkow@2525
   217
by (rtac allI 1);
nipkow@2525
   218
by (rename_tac "p" 1);
nipkow@2525
   219
by (strip_tac 1);
nipkow@2525
   220
by (rewrite_goals_tac [free_tv_subst]);
nipkow@2525
   221
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
nipkow@2525
   222
fun restrict_prems is tacf =
nipkow@2525
   223
  METAHYPS(fn prems =>
nipkow@2525
   224
    let val iprems = map (fn i => nth_elem(i,prems)) is
nipkow@2525
   225
    in cut_facts_tac iprems 1 THEN tacf 1 end);
nipkow@2525
   226
by (restrict_prems [0,4,8,9] (best_tac (!claset addEs [less_le_trans])) 1);
nipkow@1486
   227
qed_spec_mp "new_tv_W";
nipkow@1300
   228
nipkow@2525
   229
goal thy "!!sch. (v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)";
nipkow@2525
   230
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   231
by (Asm_full_simp_tac 1);
nipkow@2525
   232
by (Asm_full_simp_tac 1);
nipkow@2525
   233
by (strip_tac 1);
nipkow@2525
   234
by (rtac exI 1);
nipkow@2525
   235
by (rtac refl 1);
nipkow@2525
   236
by (Asm_full_simp_tac 1);
nipkow@2525
   237
qed_spec_mp "free_tv_bound_typ_inst1";
nipkow@2525
   238
nipkow@2525
   239
Addsimps [free_tv_bound_typ_inst1];
nipkow@1300
   240
nipkow@1300
   241
goal thy
nipkow@2525
   242
     "!n A S t m v. W e A n = Some (S,t,m) -->            \
nipkow@2525
   243
\         (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A";
nipkow@1300
   244
by (expr.induct_tac "e" 1);
nipkow@1300
   245
(* case Var n *)
nipkow@2525
   246
by (simp_tac (!simpset addsimps
nipkow@2525
   247
    [free_tv_subst] setloop (split_tac [expand_option_bind,expand_if])) 1);
nipkow@2525
   248
by (strip_tac 1);
nipkow@2525
   249
by (REPEAT (etac conjE 1));
nipkow@2525
   250
by (hyp_subst_tac 1);
nipkow@2525
   251
by (asm_full_simp_tac (!simpset addsimps [dom_def,cod_def,id_subst_def]) 1);
nipkow@2525
   252
by (case_tac "v : free_tv (nth nat A)" 1);
nipkow@2525
   253
by (Asm_full_simp_tac 1);
nipkow@2525
   254
by (strip_tac 1);
nipkow@2525
   255
by (dtac free_tv_bound_typ_inst1 1);
nipkow@2525
   256
by (simp_tac (!simpset addsimps [o_def]) 1);
nipkow@2525
   257
by (rotate_tac 3 1);
nipkow@2525
   258
by (etac exE 1);
nipkow@2525
   259
by (rotate_tac 3 1);
nipkow@2525
   260
by (Asm_full_simp_tac 1);
nipkow@2525
   261
by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
nipkow@2525
   262
by (dtac add_lessD1 1);
nipkow@2525
   263
by (fast_tac (!claset addIs [less_irrefl]) 1);
nipkow@1300
   264
(* case Abs e *)
nipkow@1300
   265
by (asm_full_simp_tac (!simpset addsimps
nipkow@2525
   266
    [free_tv_subst] setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
nipkow@1300
   267
by (strip_tac 1);
nipkow@2525
   268
by (rename_tac "S t n1 S1 t1 m v" 1);
nipkow@1300
   269
by (eres_inst_tac [("x","Suc n")] allE 1);
nipkow@2525
   270
by (eres_inst_tac [("x","FVar n # A")] allE 1);
nipkow@2525
   271
by (eres_inst_tac [("x","S")] allE 1);
nipkow@1300
   272
by (eres_inst_tac [("x","t")] allE 1);
nipkow@2525
   273
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@1300
   274
by (eres_inst_tac [("x","v")] allE 1);
nipkow@2525
   275
by (best_tac (HOL_cs addIs [cod_app_subst]
nipkow@1669
   276
                     addss (!simpset addsimps [less_Suc_eq])) 1);
nipkow@1300
   277
(* case App e1 e2 *)
nipkow@2525
   278
by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
nipkow@1300
   279
by (strip_tac 1); 
nipkow@2525
   280
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1);
nipkow@1300
   281
by (eres_inst_tac [("x","n")] allE 1);
nipkow@2525
   282
by (eres_inst_tac [("x","A")] allE 1);
nipkow@2525
   283
by (eres_inst_tac [("x","S")] allE 1);
nipkow@1300
   284
by (eres_inst_tac [("x","t")] allE 1);
nipkow@2525
   285
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@2525
   286
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@1300
   287
by (eres_inst_tac [("x","v")] allE 1);
nipkow@1300
   288
(* second case *)
nipkow@2525
   289
by (eres_inst_tac [("x","$ S A")] allE 1);
nipkow@2525
   290
by (eres_inst_tac [("x","S1")] allE 1);
nipkow@2525
   291
by (eres_inst_tac [("x","t1")] allE 1);
nipkow@2525
   292
by (eres_inst_tac [("x","n2")] allE 1);
nipkow@1300
   293
by (eres_inst_tac [("x","v")] allE 1);
nipkow@1300
   294
by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
nipkow@2525
   295
by (asm_full_simp_tac (!simpset addsimps [rotate_Some,o_def]) 1);
clasohm@1465
   296
by (dtac W_var_geD 1);
clasohm@1465
   297
by (dtac W_var_geD 1);
nipkow@1300
   298
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
nipkow@1300
   299
by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
nipkow@2525
   300
    codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
nipkow@1300
   301
    less_le_trans,less_not_refl2,subsetD]
nipkow@1300
   302
  addEs [UnE] 
nipkow@1300
   303
  addss !simpset) 1);
nipkow@1300
   304
by (Asm_full_simp_tac 1); 
clasohm@1465
   305
by (dtac (sym RS W_var_geD) 1);
clasohm@1465
   306
by (dtac (sym RS W_var_geD) 1);
nipkow@1300
   307
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
nipkow@1300
   308
by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
nipkow@2525
   309
    free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
nipkow@2525
   310
    less_le_trans,subsetD]
nipkow@2525
   311
  addEs [UnE]
nipkow@2525
   312
  addss !simpset) 1);
nipkow@2525
   313
(* LET e1 e2 *)
nipkow@2525
   314
by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
nipkow@2525
   315
by (strip_tac 1); 
nipkow@2525
   316
by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
nipkow@2525
   317
by (eres_inst_tac [("x","nat")] allE 1);
nipkow@2525
   318
by (eres_inst_tac [("x","A")] allE 1);
nipkow@2525
   319
by (eres_inst_tac [("x","S1")] allE 1);
nipkow@2525
   320
by (eres_inst_tac [("x","t1")] allE 1);
nipkow@2525
   321
by (rotate_tac 1 1);
nipkow@2525
   322
by (eres_inst_tac [("x","n2")] allE 1);
nipkow@2525
   323
by (rotate_tac 4 1);
nipkow@2525
   324
by (eres_inst_tac [("x","v")] allE 1);
nipkow@2525
   325
by (mp_tac 1);
nipkow@2525
   326
by (EVERY1 [etac allE,etac allE,etac allE,etac allE,etac allE,eres_inst_tac [("x","v")] allE]);
nipkow@2525
   327
by (mp_tac 1);
nipkow@2525
   328
by (Asm_full_simp_tac 1);
nipkow@2525
   329
by (rtac conjI 1);
nipkow@2525
   330
by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,free_tv_o_subst RS subsetD,W_var_ge] 
nipkow@2525
   331
              addDs [less_le_trans]) 1);
nipkow@2525
   332
by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,W_var_ge] 
nipkow@2525
   333
              addDs [less_le_trans]) 1);
nipkow@1486
   334
qed_spec_mp "free_tv_W"; 
nipkow@1300
   335
nipkow@2525
   336
goal thy "!!A. (!x. x : A --> x ~: B) ==> A Int B = {}";
nipkow@2525
   337
by (Fast_tac 1);
nipkow@2525
   338
qed "weaken_A_Int_B_eq_empty";
nipkow@2525
   339
nipkow@2525
   340
goal thy "!!A. x ~: A | x : B ==> x ~: A - B";
nipkow@2525
   341
by (Fast_tac 1);
nipkow@2525
   342
qed "weaken_not_elem_A_minus_B";
nipkow@2525
   343
nipkow@2525
   344
(* correctness of W with respect to has_type *)
nipkow@2525
   345
goal W.thy
nipkow@2525
   346
        "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
nipkow@2525
   347
by (expr.induct_tac "e" 1);
nipkow@2525
   348
(* case Var n *)
nipkow@2525
   349
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@2525
   350
by (strip_tac 1);
nipkow@2525
   351
by (rtac has_type.VarI 1);
nipkow@2525
   352
by (Simp_tac 1);
nipkow@2525
   353
by (simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
nipkow@2525
   354
by (rtac exI 1);
nipkow@2525
   355
by (rtac refl 1);
nipkow@2525
   356
(* case Abs e *)
nipkow@2525
   357
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
nipkow@2525
   358
                        setloop (split_tac [expand_option_bind])) 1);
nipkow@2525
   359
by (strip_tac 1);
nipkow@2525
   360
by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1);
nipkow@2525
   361
by (Asm_full_simp_tac 1);
nipkow@2525
   362
by (rtac has_type.AbsI 1);
nipkow@2525
   363
by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1);
nipkow@2525
   364
bd sym 1;
nipkow@2525
   365
by (REPEAT (etac allE 1));
nipkow@2525
   366
by (etac impE 1);
nipkow@2525
   367
by (mp_tac 2);
nipkow@2525
   368
by (Asm_simp_tac 1);
nipkow@2525
   369
ba 1;
nipkow@2525
   370
(* case App e1 e2 *)
nipkow@2525
   371
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
nipkow@2525
   372
by (strip_tac 1);
nipkow@2525
   373
by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
nipkow@2525
   374
by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1);
nipkow@2525
   375
by (res_inst_tac [("S1","S3")] (app_subst_TVar RS subst) 1);
nipkow@2525
   376
by (rtac (app_subst_Fun RS subst) 1);
nipkow@2525
   377
by (res_inst_tac [("t","$S3 (t2 -> (TVar n2))"),("s","$S3 ($S2 t1)")] subst 1);
nipkow@2525
   378
by (Asm_full_simp_tac 1);
nipkow@2525
   379
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
nipkow@2525
   380
by ((rtac (has_type_cl_sub RS spec) 1) THEN (rtac (has_type_cl_sub RS spec) 1));
nipkow@2525
   381
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
nipkow@2525
   382
by (asm_full_simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
nipkow@2525
   383
by (rtac (has_type_cl_sub RS spec) 1);
nipkow@2525
   384
by (forward_tac [new_tv_W] 1);
nipkow@2525
   385
ba 1;
nipkow@2525
   386
by (dtac conjunct1 1);
nipkow@2525
   387
by (dtac conjunct1 1);
nipkow@2525
   388
by (forward_tac [new_tv_subst_scheme_list] 1);
nipkow@2525
   389
by (rtac new_scheme_list_le 1);
nipkow@2525
   390
by (rtac W_var_ge 1);
nipkow@2525
   391
ba 1;
nipkow@2525
   392
ba 1;
nipkow@2525
   393
by (etac thin_rl 1);
nipkow@2525
   394
by (REPEAT (etac allE 1));
nipkow@2525
   395
bd sym 1;
nipkow@2525
   396
bd sym 1;
nipkow@2525
   397
by (etac thin_rl 1);
nipkow@2525
   398
by (etac thin_rl 1);
nipkow@2525
   399
by (mp_tac 1);
nipkow@2525
   400
by (mp_tac 1);
nipkow@2525
   401
ba 1;
nipkow@2525
   402
(* case Let e1 e2 *)
nipkow@2525
   403
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
nipkow@2525
   404
by (strip_tac 1);
nipkow@2525
   405
by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); 
nipkow@2525
   406
by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
nipkow@2525
   407
by (simp_tac (!simpset addsimps [o_def]) 1);
nipkow@2525
   408
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
nipkow@2525
   409
by (rtac (has_type_cl_sub RS spec) 1);
nipkow@2525
   410
by (dres_inst_tac [("x","A")] spec 1);
nipkow@2525
   411
by (dres_inst_tac [("x","S1")] spec 1);
nipkow@2525
   412
by (dres_inst_tac [("x","t1")] spec 1);
nipkow@2525
   413
by (dres_inst_tac [("x","m2")] spec 1);
nipkow@2525
   414
by (rotate_tac 4 1);
nipkow@2525
   415
by (dres_inst_tac [("x","m1")] spec 1);
nipkow@2525
   416
by (mp_tac 1);
nipkow@2525
   417
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
nipkow@2525
   418
by (simp_tac (!simpset addsimps [o_def]) 1);
nipkow@2525
   419
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
nipkow@2525
   420
by (rtac (gen_subst_commutes RS sym RS subst) 1);
nipkow@2525
   421
by (rtac (app_subst_Cons RS subst) 2);
nipkow@2525
   422
by (etac thin_rl 2);
nipkow@2525
   423
by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
nipkow@2525
   424
by (dres_inst_tac [("x","S2")] spec 2);
nipkow@2525
   425
by (dres_inst_tac [("x","t")] spec 2);
nipkow@2525
   426
by (dres_inst_tac [("x","n2")] spec 2);
nipkow@2525
   427
by (dres_inst_tac [("x","m2")] spec 2);
nipkow@2525
   428
by (forward_tac [new_tv_W] 2);
nipkow@2525
   429
ba 2;
nipkow@2525
   430
by (dtac conjunct1 2);
nipkow@2525
   431
by (dtac conjunct1 2);
nipkow@2525
   432
by (forward_tac [new_tv_subst_scheme_list] 2);
nipkow@2525
   433
by (rtac new_scheme_list_le 2);
nipkow@2525
   434
by (rtac W_var_ge 2);
nipkow@2525
   435
ba 2;
nipkow@2525
   436
ba 2;
nipkow@2525
   437
by (etac impE 2);
nipkow@2525
   438
by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
nipkow@2525
   439
by (Simp_tac 2);
nipkow@2525
   440
by (Fast_tac 2);
nipkow@2525
   441
ba 2;
nipkow@2525
   442
by (Asm_full_simp_tac 2);
nipkow@2525
   443
by (rtac weaken_A_Int_B_eq_empty 1);
nipkow@2525
   444
by (rtac allI 1);
nipkow@2525
   445
by (strip_tac 1);
nipkow@2525
   446
by (rtac weaken_not_elem_A_minus_B 1);
nipkow@2525
   447
by (case_tac "x < m2" 1);
nipkow@2525
   448
by (rtac disjI2 1);
nipkow@2525
   449
by (rtac (free_tv_gen_cons RS subst) 1);
nipkow@2525
   450
by (rtac free_tv_W 1);
nipkow@2525
   451
ba 1;
nipkow@2525
   452
by (Asm_full_simp_tac 1);
nipkow@2525
   453
ba 1;
nipkow@2525
   454
by (rtac disjI1 1);
nipkow@2525
   455
by (dtac new_tv_W 1);
nipkow@2525
   456
ba 1;
nipkow@2525
   457
by (dtac conjunct2 1);
nipkow@2525
   458
by (dtac conjunct2 1);
nipkow@2525
   459
by (rtac new_tv_not_free_tv 1);
nipkow@2525
   460
by (rtac new_tv_le 1);
nipkow@2525
   461
ba 2;
nipkow@2525
   462
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1);
nipkow@2525
   463
qed_spec_mp "W_correct_lemma";
nipkow@2525
   464
nipkow@2525
   465
goal Type.thy "new_tv n (sch::type_scheme) --> \
nipkow@2525
   466
\              $(%k.if k<n then S k else S' k) sch = $S sch";
nipkow@2525
   467
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   468
by(ALLGOALS Asm_simp_tac);
nipkow@2525
   469
qed "new_if_subst_type_scheme";
nipkow@2525
   470
Addsimps [new_if_subst_type_scheme];
nipkow@2525
   471
nipkow@2525
   472
goal Type.thy "new_tv n (A::type_scheme list) --> \
nipkow@2525
   473
\              $(%k.if k<n then S k else S' k) A = $S A";
nipkow@2525
   474
by (list.induct_tac "A" 1);
nipkow@2525
   475
by(ALLGOALS Asm_simp_tac);
nipkow@2525
   476
qed "new_if_subst_type_scheme_list";
nipkow@2525
   477
Addsimps [new_if_subst_type_scheme_list];
nipkow@2525
   478
nipkow@2525
   479
goal Arith.thy "!!n::nat. ~ k+n < n";
nipkow@2525
   480
by (nat_ind_tac "k" 1);
nipkow@2525
   481
by(ALLGOALS Asm_simp_tac);
nipkow@2525
   482
by(trans_tac 1);
nipkow@2525
   483
qed "not_add_less1";
nipkow@2525
   484
Addsimps [not_add_less1];
paulson@2083
   485
nipkow@1300
   486
(* Completeness of W w.r.t. has_type *)
nipkow@1300
   487
goal thy
nipkow@2525
   488
 "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \
nipkow@2525
   489
\             (? S t. (? m. W e A n = Some (S,t,m)) &  \
nipkow@2525
   490
\                     (? R. $S' A = $R ($S A) & t' = $R t))";
nipkow@1300
   491
by (expr.induct_tac "e" 1);
nipkow@1300
   492
(* case Var n *)
nipkow@1300
   493
by (strip_tac 1);
nipkow@1300
   494
by (simp_tac (!simpset addcongs [conj_cong] 
nipkow@2525
   495
    setloop (split_tac [expand_if])) 1);
nipkow@1300
   496
by (eresolve_tac has_type_casesE 1); 
nipkow@2525
   497
by (asm_full_simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
nipkow@2525
   498
by (etac exE 1);
nipkow@2525
   499
by (hyp_subst_tac 1);
nipkow@2525
   500
by (rename_tac "S" 1);
nipkow@2525
   501
by (res_inst_tac [("x","%x. (if x < n then S' x else S (x - n))")] exI 1);
nipkow@2525
   502
by (rtac conjI 1);
nipkow@1300
   503
by (Asm_simp_tac 1);
nipkow@2525
   504
by (asm_simp_tac (!simpset addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst] 
nipkow@2525
   505
                           delsimps [bound_typ_inst_composed_subst]) 1);
nipkow@1300
   506
nipkow@1300
   507
(* case Abs e *)
nipkow@1300
   508
by (strip_tac 1);
nipkow@1300
   509
by (eresolve_tac has_type_casesE 1);
nipkow@2525
   510
by (eres_inst_tac [("x","%x.if x=n then t1 else (S' x)")] allE 1);
nipkow@2525
   511
by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
nipkow@1300
   512
by (eres_inst_tac [("x","t2")] allE 1);
nipkow@1300
   513
by (eres_inst_tac [("x","Suc n")] allE 1);
nipkow@2525
   514
by (best_tac (HOL_cs addSDs [mk_scheme_injective] addss (!simpset addcongs [conj_cong] 
nipkow@2525
   515
    setloop (split_tac [expand_option_bind]))) 1);
nipkow@1300
   516
nipkow@1300
   517
(* case App e1 e2 *)
nipkow@1300
   518
by (strip_tac 1);
nipkow@1300
   519
by (eresolve_tac has_type_casesE 1);
nipkow@2525
   520
by (eres_inst_tac [("x","S'")] allE 1);
nipkow@2525
   521
by (eres_inst_tac [("x","A")] allE 1);
nipkow@1400
   522
by (eres_inst_tac [("x","t2 -> t'")] allE 1);
nipkow@1300
   523
by (eres_inst_tac [("x","n")] allE 1);
nipkow@1300
   524
by (safe_tac HOL_cs);
nipkow@2525
   525
by (eres_inst_tac [("x","R")] allE 1);
nipkow@2525
   526
by (eres_inst_tac [("x","$ S A")] allE 1);
nipkow@1300
   527
by (eres_inst_tac [("x","t2")] allE 1);
nipkow@1300
   528
by (eres_inst_tac [("x","m")] allE 1);
clasohm@1465
   529
by (dtac asm_rl 1);
clasohm@1465
   530
by (dtac asm_rl 1);
clasohm@1465
   531
by (dtac asm_rl 1);
nipkow@1300
   532
by (Asm_full_simp_tac 1);
nipkow@1300
   533
by (safe_tac HOL_cs);
nipkow@1300
   534
by (fast_tac HOL_cs 1);
nipkow@1300
   535
by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
nipkow@2525
   536
        conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1);
nipkow@1300
   537
nipkow@1300
   538
by (subgoal_tac
nipkow@2525
   539
  "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
nipkow@2525
   540
\        else Ra x)) ($ Sa t) = \
nipkow@2525
   541
\  $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
nipkow@2525
   542
\        else Ra x)) (ta -> (TVar ma))" 1);
nipkow@1300
   543
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
nipkow@2525
   544
\   (if x:(free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t)"),
nipkow@2525
   545
    ("s","($ Ra ta) -> t'")] ssubst 2);
nipkow@1300
   546
by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2);
clasohm@1465
   547
by (rtac eq_free_eq_subst_te 2);  
nipkow@1300
   548
by (strip_tac 2);
nipkow@1300
   549
by (subgoal_tac "na ~=ma" 2);
nipkow@1300
   550
by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
nipkow@2525
   551
    new_tv_not_free_tv,new_tv_le]) 3);
nipkow@2525
   552
by (case_tac "na:free_tv Sa" 2);
nipkow@2525
   553
(* n1 ~: free_tv S1 *)
nipkow@2525
   554
by (forward_tac [not_free_impl_id] 3);
nipkow@2525
   555
by (asm_simp_tac (!simpset 
nipkow@2525
   556
    setloop (split_tac [expand_if])) 3);
nipkow@2525
   557
(* na : free_tv Sa *)
nipkow@2525
   558
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
nipkow@2525
   559
by (dtac eq_subst_scheme_list_eq_free 2);
nipkow@1300
   560
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
nipkow@1300
   561
by (Asm_simp_tac 2); 
nipkow@2525
   562
by (case_tac "na:dom Sa" 2);
nipkow@2525
   563
(* na ~: dom Sa *)
nipkow@1300
   564
by (asm_full_simp_tac (!simpset addsimps [dom_def] 
nipkow@2525
   565
    setloop (split_tac [expand_if])) 3);
nipkow@2525
   566
(* na : dom Sa *)
clasohm@1465
   567
by (rtac eq_free_eq_subst_te 2);
nipkow@1300
   568
by (strip_tac 2);
nipkow@1300
   569
by (subgoal_tac "nb ~= ma" 2);
nipkow@1300
   570
by ((forward_tac [new_tv_W] 3) THEN (atac 3));
clasohm@1465
   571
by (etac conjE 3);
nipkow@2525
   572
by (dtac new_tv_subst_scheme_list 3);
nipkow@2525
   573
by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3);
nipkow@1300
   574
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
nipkow@2525
   575
    (!simpset addsimps [cod_def,free_tv_subst])) 3);
nipkow@1300
   576
by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
nipkow@2525
   577
    setloop (split_tac [expand_if]))) 2);
nipkow@1300
   578
by (Simp_tac 2);  
clasohm@1465
   579
by (rtac eq_free_eq_subst_te 2);
nipkow@1300
   580
by (strip_tac 2 );
nipkow@1300
   581
by (subgoal_tac "na ~= ma" 2);
nipkow@1300
   582
by ((forward_tac [new_tv_W] 3) THEN (atac 3));
clasohm@1465
   583
by (etac conjE 3);
clasohm@1465
   584
by (dtac (sym RS W_var_geD) 3);
nipkow@2525
   585
by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
nipkow@2525
   586
by (case_tac "na: free_tv t - free_tv Sa" 2);
nipkow@2525
   587
(* case na ~: free_tv t - free_tv Sa *)
nipkow@2525
   588
by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
nipkow@2525
   589
(* case na : free_tv t - free_tv Sa *)
nipkow@2525
   590
by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
nipkow@2525
   591
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
nipkow@2525
   592
by (dtac eq_subst_scheme_list_eq_free 2);
nipkow@1300
   593
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
nipkow@2525
   594
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
nipkow@2525
   595
nipkow@2525
   596
by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); 
nipkow@1300
   597
by (safe_tac HOL_cs );
nipkow@2525
   598
by (dtac mgu_Some 1);
nipkow@2525
   599
by( fast_tac (HOL_cs addss !simpset) 1);
nipkow@2525
   600
nipkow@1300
   601
by ((dtac mgu_mg 1) THEN (atac 1));
clasohm@1465
   602
by (etac exE 1);
nipkow@2525
   603
by (res_inst_tac [("x","Rb")] exI 1);
clasohm@1465
   604
by (rtac conjI 1);
nipkow@1300
   605
by (dres_inst_tac [("x","ma")] fun_cong 2);
nipkow@2525
   606
by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
nipkow@2525
   607
by (simp_tac (!simpset addsimps [subst_comp_scheme_list]) 1);
nipkow@2525
   608
by (simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym]) 1);
nipkow@2525
   609
by (res_inst_tac [("A2","($ Sa ($ S A))")] ((subst_comp_scheme_list RS sym) RSN 
nipkow@1300
   610
    (2,trans)) 1);
nipkow@2525
   611
by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
nipkow@2525
   612
by (rtac eq_free_eq_subst_scheme_list 1);
nipkow@2525
   613
by( safe_tac HOL_cs );
nipkow@1300
   614
by (subgoal_tac "ma ~= na" 1);
nipkow@1300
   615
by ((forward_tac [new_tv_W] 2) THEN (atac 2));
clasohm@1465
   616
by (etac conjE 2);
nipkow@2525
   617
by (dtac new_tv_subst_scheme_list 2);
nipkow@2525
   618
by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2);
nipkow@1486
   619
by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
clasohm@1465
   620
by (etac conjE 2);
nipkow@2525
   621
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2);
nipkow@2525
   622
by (fast_tac (set_cs addDs [W_var_geD,new_scheme_list_le,codD,
nipkow@1300
   623
    new_tv_not_free_tv]) 2);
nipkow@2525
   624
by (case_tac "na: free_tv t - free_tv Sa" 1);
nipkow@2525
   625
(* case na ~: free_tv t - free_tv Sa *)
nipkow@1300
   626
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
nipkow@2525
   627
(* case na : free_tv t - free_tv Sa *)
nipkow@1300
   628
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@2525
   629
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
nipkow@2525
   630
by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
nipkow@2525
   631
    eq_subst_scheme_list_eq_free] addss ((!simpset addsimps 
nipkow@2525
   632
    [free_tv_subst,dom_def]))) 1);
paulson@2083
   633
by (Fast_tac 1);
nipkow@2525
   634
(* case Let e1 e2 *)
nipkow@2525
   635
by (eresolve_tac has_type_casesE 1);
nipkow@2525
   636
by (eres_inst_tac [("x","S'")] allE 1);
nipkow@2525
   637
by (eres_inst_tac [("x","A")] allE 1);
nipkow@2525
   638
by (eres_inst_tac [("x","t1")] allE 1);
nipkow@2525
   639
by (eres_inst_tac [("x","n")] allE 1);
nipkow@2525
   640
by (mp_tac 1);
nipkow@2525
   641
by (mp_tac 1);
nipkow@2525
   642
by (safe_tac HOL_cs);
nipkow@2525
   643
by (Asm_simp_tac 1); 
nipkow@2525
   644
by (eres_inst_tac [("x","R")] allE 1);
nipkow@2525
   645
by (eres_inst_tac [("x","gen ($ S A) t # $ S A")] allE 1);
nipkow@2525
   646
by (eres_inst_tac [("x","t'")] allE 1);
nipkow@2525
   647
by (eres_inst_tac [("x","m")] allE 1);
nipkow@2525
   648
by (rotate_tac 4 1);
nipkow@2525
   649
by (Asm_full_simp_tac 1);
nipkow@2525
   650
by (dtac mp 1);
nipkow@2525
   651
by (rtac has_type_le_env 1);
nipkow@2525
   652
ba 1;
nipkow@2525
   653
by (Simp_tac 1);
nipkow@2525
   654
by (rtac gen_bound_typ_instance 1);
nipkow@2525
   655
by (dtac mp 1);
nipkow@2525
   656
by (forward_tac [new_tv_compatible_W] 1);
nipkow@2525
   657
by (rtac sym 1);
nipkow@2525
   658
ba 1;
nipkow@2525
   659
by (fast_tac (!claset addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1);
nipkow@2525
   660
by (safe_tac HOL_cs);
nipkow@2525
   661
by (Asm_full_simp_tac 1);
nipkow@2525
   662
by (res_inst_tac [("x","Ra")] exI 1);
nipkow@2525
   663
by (simp_tac (!simpset addsimps [o_def,subst_comp_scheme_list RS sym]) 1);
nipkow@1525
   664
qed_spec_mp "W_complete_lemma";
nipkow@1525
   665
nipkow@1525
   666
goal W.thy
nipkow@2525
   667
 "!!e. [] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
nipkow@2525
   668
\                                 (? R. t' = $ R t))";
nipkow@2525
   669
by(cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
nipkow@1525
   670
                W_complete_lemma 1);
nipkow@2525
   671
by(ALLGOALS Asm_full_simp_tac);
nipkow@1525
   672
qed "W_complete";